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 31482
 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 31475 . 2 class ZF
2 vm . . . . . . 7 setvar 𝑚
32cv 1522 . . . . . 6 class 𝑚
43wtr 4785 . . . . 5 wff Tr 𝑚
5 cgze 31469 . . . . . 6 class AxExt
6 cprv 31447 . . . . . 6 class
73, 5, 6wbr 4685 . . . . 5 wff 𝑚⊧AxExt
8 cgzp 31471 . . . . . 6 class AxPow
93, 8, 6wbr 4685 . . . . 5 wff 𝑚⊧AxPow
104, 7, 9w3a 1054 . . . 4 wff (Tr 𝑚𝑚⊧AxExt ∧ 𝑚⊧AxPow)
11 cgzu 31472 . . . . . 6 class AxUn
123, 11, 6wbr 4685 . . . . 5 wff 𝑚⊧AxUn
13 cgzg 31473 . . . . . 6 class AxReg
143, 13, 6wbr 4685 . . . . 5 wff 𝑚⊧AxReg
15 cgzi 31474 . . . . . 6 class AxInf
163, 15, 6wbr 4685 . . . . 5 wff 𝑚⊧AxInf
1712, 14, 16w3a 1054 . . . 4 wff (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf)
18 vu . . . . . . . 8 setvar 𝑢
1918cv 1522 . . . . . . 7 class 𝑢
20 cgzr 31470 . . . . . . 7 class AxRep
2119, 20cfv 5926 . . . . . 6 class (AxRep‘𝑢)
223, 21, 6wbr 4685 . . . . 5 wff 𝑚⊧(AxRep‘𝑢)
23 com 7107 . . . . . 6 class ω
24 cfmla 31445 . . . . . 6 class Fmla
2523, 24cfv 5926 . . . . 5 class (Fmla‘ω)
2622, 18, 25wral 2941 . . . 4 wff 𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢)
2710, 17, 26w3a 1054 . . 3 wff ((Tr 𝑚𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))
2827, 2cab 2637 . 2 class {𝑚 ∣ ((Tr 𝑚𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))}
291, 28wceq 1523 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