Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gzinf Unicode version

Definition df-gzinf 23956
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
StepHypRef Expression
1 cgzi 23949 . 2  class  AxInf
2 c0 3455 . . . . 5  class  (/)
3 c1o 6472 . . . . 5  class  1o
4 cgoe 23916 . . . . 5  class  e.g
52, 3, 4co 5858 . . . 4  class  ( (/)  e.g 
1o )
6 c2o 6473 . . . . . . 7  class  2o
76, 3, 4co 5858 . . . . . 6  class  ( 2o 
e.g  1o )
86, 2, 4co 5858 . . . . . . . 8  class  ( 2o 
e.g  (/) )
9 cgoa 23930 . . . . . . . 8  class  /\g
108, 5, 9co 5858 . . . . . . 7  class  ( ( 2o  e.g  (/) )  /\g  ( (/)  e.g  1o )
)
1110, 2cgox 23935 . . . . . 6  class  E.g (/) ( ( 2o  e.g  (/) )  /\g  ( (/)  e.g  1o )
)
12 cgoi 23931 . . . . . 6  class  ->g
137, 11, 12co 5858 . . . . 5  class  ( ( 2o  e.g  1o ) 
->g  E.g (/) ( ( 2o 
e.g  (/) )  /\g  ( (/) 
e.g  1o ) ) )
1413, 6cgol 23918 . . . 4  class  A.g 2o ( ( 2o  e.g  1o )  ->g  E.g (/) ( ( 2o  e.g  (/) )  /\g  ( (/)  e.g  1o )
) )
155, 14, 9co 5858 . . 3  class  ( (
(/)  e.g  1o )  /\g  A.g
2o ( ( 2o 
e.g  1o )  ->g  E.g (/) ( ( 2o  e.g  (/) )  /\g  ( (/)  e.g  1o )
) ) )
1615, 3cgox 23935 . 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 ) ) ) )
171, 16wceq 1623 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 ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator