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

Definition df-gzrep 23952
Description: The Godel-set version of the Axiom Scheme of Replacement. Since this is a scheme and not a single axiom, it manifests as a function on wffs, each giving rise to a different axiom. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-gzrep  |-  AxRep  =  ( u  e.  ( Fmla `  om )  |->  ( A.g 3o E.g 1o A.g 2o ( A.g 1o u  ->g  ( 2o  =g  1o ) )  ->g  A.g 1o A.g 2o ( ( 2o  e.g  1o )  <->g  E.g 3o ( ( 3o  e.g  (/) )  /\g  A.g
1o u ) ) ) )

Detailed syntax breakdown of Definition df-gzrep
StepHypRef Expression
1 cgzr 23945 . 2  class  AxRep
2 vu . . 3  set  u
3 com 4656 . . . 4  class  om
4 cfmla 23920 . . . 4  class  Fmla
53, 4cfv 5255 . . 3  class  ( Fmla `  om )
62cv 1622 . . . . . . . . 9  class  u
7 c1o 6472 . . . . . . . . 9  class  1o
86, 7cgol 23918 . . . . . . . 8  class  A.g 1o u
9 c2o 6473 . . . . . . . . 9  class  2o
10 cgoq 23934 . . . . . . . . 9  class  =g
119, 7, 10co 5858 . . . . . . . 8  class  ( 2o 
=g  1o )
12 cgoi 23931 . . . . . . . 8  class  ->g
138, 11, 12co 5858 . . . . . . 7  class  ( A.g 1o u  ->g  ( 2o 
=g  1o ) )
1413, 9cgol 23918 . . . . . 6  class  A.g 2o ( A.g 1o u  ->g  ( 2o  =g  1o ) )
1514, 7cgox 23935 . . . . 5  class  E.g 1o A.g
2o ( A.g 1o u  ->g  ( 2o  =g  1o ) )
16 c3o 6474 . . . . 5  class  3o
1715, 16cgol 23918 . . . 4  class  A.g 3o E.g
1o A.g 2o ( A.g 1o u  ->g  ( 2o 
=g  1o ) )
18 cgoe 23916 . . . . . . . 8  class  e.g
199, 7, 18co 5858 . . . . . . 7  class  ( 2o 
e.g  1o )
20 c0 3455 . . . . . . . . . 10  class  (/)
2116, 20, 18co 5858 . . . . . . . . 9  class  ( 3o 
e.g  (/) )
22 cgoa 23930 . . . . . . . . 9  class  /\g
2321, 8, 22co 5858 . . . . . . . 8  class  ( ( 3o  e.g  (/) )  /\g  A.g
1o u )
2423, 16cgox 23935 . . . . . . 7  class  E.g 3o ( ( 3o  e.g  (/) )  /\g  A.g 1o u
)
25 cgob 23933 . . . . . . 7  class  <->g
2619, 24, 25co 5858 . . . . . 6  class  ( ( 2o  e.g  1o ) 
<->g  E.g 3o ( ( 3o 
e.g  (/) )  /\g  A.g 1o u ) )
2726, 9cgol 23918 . . . . 5  class  A.g 2o ( ( 2o  e.g  1o )  <->g  E.g 3o ( ( 3o  e.g  (/) )  /\g  A.g
1o u ) )
2827, 7cgol 23918 . . . 4  class  A.g 1o A.g
2o ( ( 2o 
e.g  1o )  <->g  E.g 3o ( ( 3o  e.g  (/) )  /\g  A.g 1o u
) )
2917, 28, 12co 5858 . . 3  class  ( A.g 3o E.g 1o A.g 2o ( A.g 1o u  ->g  ( 2o  =g  1o ) )  ->g  A.g 1o A.g 2o ( ( 2o  e.g  1o )  <->g  E.g 3o ( ( 3o  e.g  (/) )  /\g  A.g
1o u ) ) )
302, 5, 29cmpt 4077 . 2  class  ( u  e.  ( Fmla `  om )  |->  ( A.g 3o E.g
1o A.g 2o ( A.g 1o u  ->g  ( 2o 
=g  1o ) ) 
->g  A.g 1o A.g 2o ( ( 2o  e.g  1o )  <->g  E.g 3o ( ( 3o  e.g  (/) )  /\g  A.g
1o u ) ) ) )
311, 30wceq 1623 1  wff  AxRep  =  ( u  e.  ( Fmla `  om )  |->  ( A.g 3o E.g 1o A.g 2o ( A.g 1o u  ->g  ( 2o  =g  1o ) )  ->g  A.g 1o A.g 2o ( ( 2o  e.g  1o )  <->g  E.g 3o ( ( 3o  e.g  (/) )  /\g  A.g
1o u ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator