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

Definition df-gzinf 23971
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 23964 . 2  class  AxInf
2 c0 3468 . . . . 5  class  (/)
3 c1o 6488 . . . . 5  class  1o
4 cgoe 23931 . . . . 5  class  e.g
52, 3, 4co 5874 . . . 4  class  ( (/)  e.g 
1o )
6 c2o 6489 . . . . . . 7  class  2o
76, 3, 4co 5874 . . . . . 6  class  ( 2o 
e.g  1o )
86, 2, 4co 5874 . . . . . . . 8  class  ( 2o 
e.g  (/) )
9 cgoa 23945 . . . . . . . 8  class  /\g
108, 5, 9co 5874 . . . . . . 7  class  ( ( 2o  e.g  (/) )  /\g  ( (/)  e.g  1o )
)
1110, 2cgox 23950 . . . . . 6  class  E.g (/) ( ( 2o  e.g  (/) )  /\g  ( (/)  e.g  1o )
)
12 cgoi 23946 . . . . . 6  class  ->g
137, 11, 12co 5874 . . . . 5  class  ( ( 2o  e.g  1o ) 
->g  E.g (/) ( ( 2o 
e.g  (/) )  /\g  ( (/) 
e.g  1o ) ) )
1413, 6cgol 23933 . . . 4  class  A.g 2o ( ( 2o  e.g  1o )  ->g  E.g (/) ( ( 2o  e.g  (/) )  /\g  ( (/)  e.g  1o )
) )
155, 14, 9co 5874 . . 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 23950 . 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 1632 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