Metamath Proof Explorer

Definition df-gzreg

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

Ref Expression
Assertion df-gzreg 
|- AxReg = ( E.g 1o ( 1o e.g (/) ) ->g E.g 1o ( ( 1o e.g (/) ) /\g A.g 2o ( ( 2o e.g 1o ) ->g -.g ( 2o e.g (/) ) ) ) )

Detailed syntax breakdown

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