Definition df-gzinf 31355

Description: The Godel-set version of the Axiom of Infinity. (Contributed by Mario Carneiro, 14-Jul-2013.)

Assertion

Ref	Expression
df-gzinf	|- AxInf = E.g 1o ( ( (/) e.g 1o ) /\g A.g 2o ( ( 2o e.g 1o ) ->g E.g (/) ( ( 2o e.g (/) ) /\g ( (/) e.g 1o ) ) ) )

Detailed syntax breakdown of Definition df-gzinf

Step	Hyp	Ref	Expression
1		cgzi 31348	. 2 class AxInf
2		c0 3915	. . . . 5 class (/)
3		c1o 7553	. . . . 5 class 1o
4		cgoe 31315	. . . . 5 class e.g
5	2, 3, 4	co 6650	. . . 4 class ( (/) e.g 1o )
6		c2o 7554	. . . . . . 7 class 2o
7	6, 3, 4	co 6650	. . . . . 6 class ( 2o e.g 1o )
8	6, 2, 4	co 6650	. . . . . . . 8 class ( 2o e.g (/) )
9		cgoa 31329	. . . . . . . 8 class /\g
10	8, 5, 9	co 6650	. . . . . . 7 class ( ( 2o e.g (/) ) /\g ( (/) e.g 1o ) )
11	10, 2	cgox 31334	. . . . . 6 class E.g (/) ( ( 2o e.g (/) ) /\g ( (/) e.g 1o ) )
12		cgoi 31330	. . . . . 6 class ->g
13	7, 11, 12	co 6650	. . . . 5 class ( ( 2o e.g 1o ) ->g E.g (/) ( ( 2o e.g (/) ) /\g ( (/) e.g 1o ) ) )
14	13, 6	cgol 31317	. . . 4 class A.g 2o ( ( 2o e.g 1o ) ->g E.g (/) ( ( 2o e.g (/) ) /\g ( (/) e.g 1o ) ) )
15	5, 14, 9	co 6650	. . 3 class ( ( (/) e.g 1o ) /\g A.g 2o ( ( 2o e.g 1o ) ->g E.g (/) ( ( 2o e.g (/) ) /\g ( (/) e.g 1o ) ) ) )
16	15, 3	cgox 31334	. 2 class E.g 1o ( ( (/) e.g 1o ) /\g A.g 2o ( ( 2o e.g 1o ) ->g E.g (/) ( ( 2o e.g (/) ) /\g ( (/) e.g 1o ) ) ) )
17	1, 16	wceq 1483	1 wff AxInf = E.g 1o ( ( (/) e.g 1o ) /\g A.g 2o ( ( 2o e.g 1o ) ->g E.g (/) ( ( 2o e.g (/) ) /\g ( (/) e.g 1o ) ) ) )

This definition is referenced by: (None)