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 ∧ ∀ u ∈ Fmla ⁡ ω m ⊧ AxRep ⁡ u

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgzf class ZF
1 vm setvar m
2 1 cv setvar m
3 2 wtr wff Tr ⁡ m
4 cprv class ⊧
5 cgze class AxExt
6 2 5 4 wbr wff m ⊧ AxExt
7 cgzp class AxPow
8 2 7 4 wbr wff m ⊧ AxPow
9 3 6 8 w3a wff Tr ⁡ m ∧ m ⊧ AxExt ∧ m ⊧ AxPow
10 cgzu class AxUn
11 2 10 4 wbr wff m ⊧ AxUn
12 cgzg class AxReg
13 2 12 4 wbr wff m ⊧ AxReg
14 cgzi class AxInf
15 2 14 4 wbr wff m ⊧ AxInf
16 11 13 15 w3a wff m ⊧ AxUn ∧ m ⊧ AxReg ∧ m ⊧ AxInf
17 vu setvar u
18 cfmla class Fmla
19 com class ω
20 19 18 cfv class Fmla ⁡ ω
21 cgzr class AxRep
22 17 cv setvar u
23 22 21 cfv class AxRep ⁡ u
24 2 23 4 wbr wff m ⊧ AxRep ⁡ u
25 24 17 20 wral wff ∀ u ∈ Fmla ⁡ ω m ⊧ AxRep ⁡ u
26 9 16 25 w3a wff Tr ⁡ m ∧ m ⊧ AxExt ∧ m ⊧ AxPow ∧ m ⊧ AxUn ∧ m ⊧ AxReg ∧ m ⊧ AxInf ∧ ∀ u ∈ Fmla ⁡ ω m ⊧ AxRep ⁡ u
27 26 1 cab class m | Tr ⁡ m ∧ m ⊧ AxExt ∧ m ⊧ AxPow ∧ m ⊧ AxUn ∧ m ⊧ AxReg ∧ m ⊧ AxInf ∧ ∀ u ∈ Fmla ⁡ ω m ⊧ AxRep ⁡ u
28 0 27 wceq wff ZF = m | Tr ⁡ m ∧ m ⊧ AxExt ∧ m ⊧ AxPow ∧ m ⊧ AxUn ∧ m ⊧ AxReg ∧ m ⊧ AxInf ∧ ∀ u ∈ Fmla ⁡ ω m ⊧ AxRep ⁡ u