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

Definition df-gzinf 25060
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 25053 . 2  class  AxInf
2 c0 3628 . . . . 5  class  (/)
3 c1o 6717 . . . . 5  class  1o
4 cgoe 25020 . . . . 5  class  e.g
52, 3, 4co 6081 . . . 4  class  ( (/)  e.g 
1o )
6 c2o 6718 . . . . . . 7  class  2o
76, 3, 4co 6081 . . . . . 6  class  ( 2o 
e.g  1o )
86, 2, 4co 6081 . . . . . . . 8  class  ( 2o 
e.g  (/) )
9 cgoa 25034 . . . . . . . 8  class  /\g
108, 5, 9co 6081 . . . . . . 7  class  ( ( 2o  e.g  (/) )  /\g  ( (/)  e.g  1o )
)
1110, 2cgox 25039 . . . . . 6  class  E.g (/) ( ( 2o  e.g  (/) )  /\g  ( (/)  e.g  1o )
)
12 cgoi 25035 . . . . . 6  class  ->g
137, 11, 12co 6081 . . . . 5  class  ( ( 2o  e.g  1o ) 
->g  E.g (/) ( ( 2o 
e.g  (/) )  /\g  ( (/) 
e.g  1o ) ) )
1413, 6cgol 25022 . . . 4  class  A.g 2o ( ( 2o  e.g  1o )  ->g  E.g (/) ( ( 2o  e.g  (/) )  /\g  ( (/)  e.g  1o )
) )
155, 14, 9co 6081 . . 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 25039 . 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 1652 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