Definition df-fo 195

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

Assertion

Ref	Expression
df-fo	|- T. |= [onto = \f:(al -> be) (A.\y:be (E.\x:al [y:be = (f:(al -> be)x:al)]))]

Distinct variable group:   x,f,y

Detailed syntax breakdown of Definition df-fo

Step	Hyp	Ref	Expression
1		kt 8	. 2 term T.
2		tfo 190	. . 3 term onto
3		hal	. . . . 5 type al
4		hbe	. . . . 5 type be
5	3, 4	ht 2	. . . 4 type (al -> be)
6		vf	. . . 4 var f
7		tal 122	. . . . 5 term A.
8		vy	. . . . . 6 var y
9		tex 123	. . . . . . 7 term E.
10		vx	. . . . . . . 8 var x
11	4, 8	tv 1	. . . . . . . . 9 term y:be
12	5, 6	tv 1	. . . . . . . . . 10 term f:(al -> be)
13	3, 10	tv 1	. . . . . . . . . 10 term x:al
14	12, 13	kc 5	. . . . . . . . 9 term (f:(al -> be)x:al)
15		ke 7	. . . . . . . . 9 term =
16	11, 14, 15	kbr 9	. . . . . . . 8 term [y:be = (f:(al -> be)x:al)]
17	3, 10, 16	kl 6	. . . . . . 7 term \x:al [y:be = (f:(al -> be)x:al)]
18	9, 17	kc 5	. . . . . 6 term (E.\x:al [y:be = (f:(al -> be)x:al)])
19	4, 8, 18	kl 6	. . . . 5 term \y:be (E.\x:al [y:be = (f:(al -> be)x:al)])
20	7, 19	kc 5	. . . 4 term (A.\y:be (E.\x:al [y:be = (f:(al -> be)x:al)]))
21	5, 6, 20	kl 6	. . 3 term \f:(al -> be) (A.\y:be (E.\x:al [y:be = (f:(al -> be)x:al)]))
22	2, 21, 15	kbr 9	. 2 term [onto = \f:(al -> be) (A.\y:be (E.\x:al [y:be = (f:(al -> be)x:al)]))]
23	1, 22	wffMMJ2 11	1 wff T. |= [onto = \f:(al -> be) (A.\y:be (E.\x:al [y:be = (f:(al -> be)x:al)]))]

This definition is referenced by: (None)