Metamath Proof Explorer

Definition df-gzinf

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

Ref Expression
Assertion 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

Step Hyp Ref Expression
0 cgzi 
 |-  AxInf
1 c1o 
 |-  1o
2 c0 
 |-  (/)
3 cgoe 
 |-  e.g
4 2 1 3 co 
 |-  ( (/) e.g 1o )
5 cgoa 
 |-  /\g
6 c2o 
 |-  2o
7 6 1 3 co 
 |-  ( 2o e.g 1o )
8 cgoi 
 |-  ->g
9 6 2 3 co 
 |-  ( 2o e.g (/) )
10 9 4 5 co 
 |-  ( ( 2o e.g (/) ) /\g ( (/) e.g 1o ) )
11 10 2 cgox 
 |-  E.g (/) ( ( 2o e.g (/) ) /\g ( (/) e.g 1o ) )
12 7 11 8 co 
 |-  ( ( 2o e.g 1o ) ->g E.g (/) ( ( 2o e.g (/) ) /\g ( (/) e.g 1o ) ) )
13 12 6 cgol 
 |-  A.g 2o ( ( 2o e.g 1o ) ->g E.g (/) ( ( 2o e.g (/) ) /\g ( (/) e.g 1o ) ) )
14 4 13 5 co 
 |-  ( ( (/) e.g 1o ) /\g A.g 2o ( ( 2o e.g 1o ) ->g E.g (/) ( ( 2o e.g (/) ) /\g ( (/) e.g 1o ) ) ) )
15 14 1 cgox 
 |-  E.g 1o ( ( (/) e.g 1o ) /\g A.g 2o ( ( 2o e.g 1o ) ->g E.g (/) ( ( 2o e.g (/) ) /\g ( (/) e.g 1o ) ) ) )
16 0 15 wceq 
 |-  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 ) ) ) )