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 30412
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 30405 . 2 class ZF
2 vm . . . . . . 7 setvar 𝑚
32cv 1473 . . . . . 6 class 𝑚
43wtr 4670 . . . . 5 wff Tr 𝑚
5 cgze 30399 . . . . . 6 class AxExt
6 cprv 30377 . . . . . 6 class
73, 5, 6wbr 4573 . . . . 5 wff 𝑚⊧AxExt
8 cgzp 30401 . . . . . 6 class AxPow
93, 8, 6wbr 4573 . . . . 5 wff 𝑚⊧AxPow
104, 7, 9w3a 1030 . . . 4 wff (Tr 𝑚𝑚⊧AxExt ∧ 𝑚⊧AxPow)
11 cgzu 30402 . . . . . 6 class AxUn
123, 11, 6wbr 4573 . . . . 5 wff 𝑚⊧AxUn
13 cgzg 30403 . . . . . 6 class AxReg
143, 13, 6wbr 4573 . . . . 5 wff 𝑚⊧AxReg
15 cgzi 30404 . . . . . 6 class AxInf
163, 15, 6wbr 4573 . . . . 5 wff 𝑚⊧AxInf
1712, 14, 16w3a 1030 . . . 4 wff (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf)
18 vu . . . . . . . 8 setvar 𝑢
1918cv 1473 . . . . . . 7 class 𝑢
20 cgzr 30400 . . . . . . 7 class AxRep
2119, 20cfv 5786 . . . . . 6 class (AxRep‘𝑢)
223, 21, 6wbr 4573 . . . . 5 wff 𝑚⊧(AxRep‘𝑢)
23 com 6930 . . . . . 6 class ω
24 cfmla 30375 . . . . . 6 class Fmla
2523, 24cfv 5786 . . . . 5 class (Fmla‘ω)
2622, 18, 25wral 2891 . . . 4 wff 𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢)
2710, 17, 26w3a 1030 . . 3 wff ((Tr 𝑚𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))
2827, 2cab 2591 . 2 class {𝑚 ∣ ((Tr 𝑚𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))}
291, 28wceq 1474 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