Definition df-fo 195

Description: Define an onto function. (Contributed by Mario Carneiro, 10-Oct-2014.)

Assertion

Ref	Expression
df-fo	⊢ ⊤⊧[onto = λf:(α → β) (∀λy:β (∃λx:α [y:β = (f:(α → β)x:α)]))]

Distinct variable group:   x,f,y

Detailed syntax breakdown of Definition df-fo

Step	Hyp	Ref	Expression
1		kt 8	. 2 term ⊤
2		tfo 190	. . 3 term onto
3		hal	. . . . 5 type α
4		hbe	. . . . 5 type β
5	3, 4	ht 2	. . . 4 type (α → β)
6		vf	. . . 4 var f
7		tal 122	. . . . 5 term ∀
8		vy	. . . . . 6 var y
9		tex 123	. . . . . . 7 term ∃
10		vx	. . . . . . . 8 var x
11	4, 8	tv 1	. . . . . . . . 9 term y:β
12	5, 6	tv 1	. . . . . . . . . 10 term f:(α → β)
13	3, 10	tv 1	. . . . . . . . . 10 term x:α
14	12, 13	kc 5	. . . . . . . . 9 term (f:(α → β)x:α)
15		ke 7	. . . . . . . . 9 term =
16	11, 14, 15	kbr 9	. . . . . . . 8 term [y:β = (f:(α → β)x:α)]
17	3, 10, 16	kl 6	. . . . . . 7 term λx:α [y:β = (f:(α → β)x:α)]
18	9, 17	kc 5	. . . . . 6 term (∃λx:α [y:β = (f:(α → β)x:α)])
19	4, 8, 18	kl 6	. . . . 5 term λy:β (∃λx:α [y:β = (f:(α → β)x:α)])
20	7, 19	kc 5	. . . 4 term (∀λy:β (∃λx:α [y:β = (f:(α → β)x:α)]))
21	5, 6, 20	kl 6	. . 3 term λf:(α → β) (∀λy:β (∃λx:α [y:β = (f:(α → β)x:α)]))
22	2, 21, 15	kbr 9	. 2 term [onto = λf:(α → β) (∀λy:β (∃λx:α [y:β = (f:(α → β)x:α)]))]
23	1, 22	wffMMJ2 11	1 wff ⊤⊧[onto = λf:(α → β) (∀λy:β (∃λx:α [y:β = (f:(α → β)x:α)]))]

This definition is referenced by: (None)