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

Definition df-gzf 32603
Description: Define the class of all (transitive) models of ZF. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-gzf ZF = {𝑚 ∣ ((Tr 𝑚𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))}
Distinct variable group:   𝑢,𝑚

Detailed syntax breakdown of Definition df-gzf
StepHypRef Expression
1 cgzf 32596 . 2 class ZF
2 vm . . . . . . 7 setvar 𝑚
32cv 1527 . . . . . 6 class 𝑚
43wtr 5163 . . . . 5 wff Tr 𝑚
5 cgze 32590 . . . . . 6 class AxExt
6 cprv 32483 . . . . . 6 class
73, 5, 6wbr 5057 . . . . 5 wff 𝑚⊧AxExt
8 cgzp 32592 . . . . . 6 class AxPow
93, 8, 6wbr 5057 . . . . 5 wff 𝑚⊧AxPow
104, 7, 9w3a 1079 . . . 4 wff (Tr 𝑚𝑚⊧AxExt ∧ 𝑚⊧AxPow)
11 cgzu 32593 . . . . . 6 class AxUn
123, 11, 6wbr 5057 . . . . 5 wff 𝑚⊧AxUn
13 cgzg 32594 . . . . . 6 class AxReg
143, 13, 6wbr 5057 . . . . 5 wff 𝑚⊧AxReg
15 cgzi 32595 . . . . . 6 class AxInf
163, 15, 6wbr 5057 . . . . 5 wff 𝑚⊧AxInf
1712, 14, 16w3a 1079 . . . 4 wff (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf)
18 vu . . . . . . . 8 setvar 𝑢
1918cv 1527 . . . . . . 7 class 𝑢
20 cgzr 32591 . . . . . . 7 class AxRep
2119, 20cfv 6348 . . . . . 6 class (AxRep‘𝑢)
223, 21, 6wbr 5057 . . . . 5 wff 𝑚⊧(AxRep‘𝑢)
23 com 7569 . . . . . 6 class ω
24 cfmla 32481 . . . . . 6 class Fmla
2523, 24cfv 6348 . . . . 5 class (Fmla‘ω)
2622, 18, 25wral 3135 . . . 4 wff 𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢)
2710, 17, 26w3a 1079 . . 3 wff ((Tr 𝑚𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))
2827, 2cab 2796 . 2 class {𝑚 ∣ ((Tr 𝑚𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))}
291, 28wceq 1528 1 wff ZF = {𝑚 ∣ ((Tr 𝑚𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))}
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator