Definition df-fv 282

Description: Definition of function application. This sends a temporary communication channel a to F, and communicates the input X and output y. Compare with df-la 280 to see how functions are defined.

Assertion

Ref	Expression
df-fv	⊦ (F' X) = {r | νa[F ≪ a] [a ≪ X] [a ≫ y] [r ≪ y] 1}

Distinct variable groups:   a,r,y,F   r,X,a,y

Detailed syntax breakdown of Definition df-fv

Step	Hyp	Ref	Expression
1		nf	. . 3 nilad F
2		nx	. . 3 nilad X
3	1, 2	nfv 281	. 2 nilad (F' X)
4		wone 103	. . . . . . . 8 wff 1
5		vr	. . . . . . . . 9 var r
6	5	nvar 203	. . . . . . . 8 nilad r
7		vy	. . . . . . . . 9 var y
8	7	nvar 203	. . . . . . . 8 nilad y
9	4, 6, 8	wse 204	. . . . . . 7 wff [r ≪ y] 1
10		va	. . . . . . . 8 var a
11	10	nvar 203	. . . . . . 7 nilad a
12	9, 7, 11	wre 205	. . . . . 6 wff [a ≫ y] [r ≪ y] 1
13	12, 11, 2	wse 204	. . . . 5 wff [a ≪ X] [a ≫ y] [r ≪ y] 1
14	13, 1, 11	wse 204	. . . 4 wff [F ≪ a] [a ≪ X] [a ≫ y] [r ≪ y] 1
15	14, 10	wnu 206	. . 3 wff νa[F ≪ a] [a ≪ X] [a ≫ y] [r ≪ y] 1
16	15, 5	nnab 266	. 2 nilad {r | νa[F ≪ a] [a ≪ X] [a ≫ y] [r ≪ y] 1}
17	3, 16	weq 246	1 wff (F' X) = {r | νa[F ≪ a] [a ≪ X] [a ≫ y] [r ≪ y] 1}

This definition is referenced by: (None)