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

Definition df-gzf 23957
Description: Define the class of all (transitive) models of ZF. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-gzf  |-  ZF  =  { m  |  (
( Tr  m  /\  m  |=  AxExt  /\  m  |=  AxPow
)  /\  ( m  |=  AxUn  /\  m  |=  AxReg  /\  m  |=  AxInf )  /\  A. u  e.  ( Fmla `  om ) m  |=  ( AxRep `  u )
) }
Distinct variable group:    u, m

Detailed syntax breakdown of Definition df-gzf
StepHypRef Expression
1 cgzf 23950 . 2  class  ZF
2 vm . . . . . . 7  set  m
32cv 1622 . . . . . 6  class  m
43wtr 4113 . . . . 5  wff  Tr  m
5 cgze 23944 . . . . . 6  class  AxExt
6 cprv 23922 . . . . . 6  class  |=
73, 5, 6wbr 4023 . . . . 5  wff  m  |=  AxExt
8 cgzp 23946 . . . . . 6  class  AxPow
93, 8, 6wbr 4023 . . . . 5  wff  m  |=  AxPow
104, 7, 9w3a 934 . . . 4  wff  ( Tr  m  /\  m  |=  AxExt  /\  m  |=  AxPow )
11 cgzu 23947 . . . . . 6  class  AxUn
123, 11, 6wbr 4023 . . . . 5  wff  m  |=  AxUn
13 cgzg 23948 . . . . . 6  class  AxReg
143, 13, 6wbr 4023 . . . . 5  wff  m  |=  AxReg
15 cgzi 23949 . . . . . 6  class  AxInf
163, 15, 6wbr 4023 . . . . 5  wff  m  |=  AxInf
1712, 14, 16w3a 934 . . . 4  wff  ( m 
|=  AxUn  /\  m  |=  AxReg  /\  m  |=  AxInf )
18 vu . . . . . . . 8  set  u
1918cv 1622 . . . . . . 7  class  u
20 cgzr 23945 . . . . . . 7  class  AxRep
2119, 20cfv 5255 . . . . . 6  class  ( AxRep `  u )
223, 21, 6wbr 4023 . . . . 5  wff  m  |=  ( AxRep `  u )
23 com 4656 . . . . . 6  class  om
24 cfmla 23920 . . . . . 6  class  Fmla
2523, 24cfv 5255 . . . . 5  class  ( Fmla `  om )
2622, 18, 25wral 2543 . . . 4  wff  A. u  e.  ( Fmla `  om ) m  |=  ( AxRep `  u )
2710, 17, 26w3a 934 . . 3  wff  ( ( Tr  m  /\  m  |=  AxExt  /\  m  |=  AxPow
)  /\  ( m  |=  AxUn  /\  m  |=  AxReg  /\  m  |=  AxInf )  /\  A. u  e.  ( Fmla `  om ) m  |=  ( AxRep `  u )
)
2827, 2cab 2269 . 2  class  { m  |  ( ( Tr  m  /\  m  |=  AxExt  /\  m  |=  AxPow )  /\  ( m  |=  AxUn  /\  m  |=  AxReg  /\  m  |=  AxInf
)  /\  A. u  e.  ( Fmla `  om ) m  |=  ( AxRep `  u ) ) }
291, 28wceq 1623 1  wff  ZF  =  { m  |  (
( Tr  m  /\  m  |=  AxExt  /\  m  |=  AxPow
)  /\  ( m  |=  AxUn  /\  m  |=  AxReg  /\  m  |=  AxInf )  /\  A. u  e.  ( Fmla `  om ) m  |=  ( AxRep `  u )
) }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator