Metamath Proof Explorer

Definition df-gzf

Description: Define the class of all (transitive) models of ZF. (Contributed by Mario Carneiro, 14-Jul-2013)

Ref Expression
Assertion df-gzf 
|- ZF = { m | ( ( Tr m /\ m |= AxExt /\ m |= AxPow ) /\ ( m |= AxUn /\ m |= AxReg /\ m |= AxInf ) /\ A. u e. ( Fmla ` _om ) m |= ( AxRep ` u ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgzf 
 |-  ZF
1 vm 
 |-  m
2 1 cv 
 |-  m
3 2 wtr 
 |-  Tr m
4 cprv 
 |-  |=
5 cgze 
 |-  AxExt
6 2 5 4 wbr 
 |-  m |= AxExt
7 cgzp 
 |-  AxPow
8 2 7 4 wbr 
 |-  m |= AxPow
9 3 6 8 w3a 
 |-  ( Tr m /\ m |= AxExt /\ m |= AxPow )
10 cgzu 
 |-  AxUn
11 2 10 4 wbr 
 |-  m |= AxUn
12 cgzg 
 |-  AxReg
13 2 12 4 wbr 
 |-  m |= AxReg
14 cgzi 
 |-  AxInf
15 2 14 4 wbr 
 |-  m |= AxInf
16 11 13 15 w3a 
 |-  ( m |= AxUn /\ m |= AxReg /\ m |= AxInf )
17 vu 
 |-  u
18 cfmla 
 |-  Fmla
19 com 
 |-  _om
20 19 18 cfv 
 |-  ( Fmla ` _om )
21 cgzr 
 |-  AxRep
22 17 cv 
 |-  u
23 22 21 cfv 
 |-  ( AxRep ` u )
24 2 23 4 wbr 
 |-  m |= ( AxRep ` u )
25 24 17 20 wral 
 |-  A. u e. ( Fmla ` _om ) m |= ( AxRep ` u )
26 9 16 25 w3a 
 |-  ( ( Tr m /\ m |= AxExt /\ m |= AxPow ) /\ ( m |= AxUn /\ m |= AxReg /\ m |= AxInf ) /\ A. u e. ( Fmla ` _om ) m |= ( AxRep ` u ) )
27 26 1 cab 
 |-  { m | ( ( Tr m /\ m |= AxExt /\ m |= AxPow ) /\ ( m |= AxUn /\ m |= AxReg /\ m |= AxInf ) /\ A. u e. ( Fmla ` _om ) m |= ( AxRep ` u ) ) }
28 0 27 wceq 
 |-  ZF = { m | ( ( Tr m /\ m |= AxExt /\ m |= AxPow ) /\ ( m |= AxUn /\ m |= AxReg /\ m |= AxInf ) /\ A. u e. ( Fmla ` _om ) m |= ( AxRep ` u ) ) }