Step | Hyp | Ref
| Expression |
1 | | cgzf 34110 |
. 2
class ZF |
2 | | vm |
. . . . . . 7
setvar 𝑚 |
3 | 2 | cv 1541 |
. . . . . 6
class 𝑚 |
4 | 3 | wtr 5226 |
. . . . 5
wff Tr 𝑚 |
5 | | cgze 34104 |
. . . . . 6
class
AxExt |
6 | | cprv 33997 |
. . . . . 6
class
⊧ |
7 | 3, 5, 6 | wbr 5109 |
. . . . 5
wff 𝑚⊧AxExt |
8 | | cgzp 34106 |
. . . . . 6
class
AxPow |
9 | 3, 8, 6 | wbr 5109 |
. . . . 5
wff 𝑚⊧AxPow |
10 | 4, 7, 9 | w3a 1088 |
. . . 4
wff (Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow) |
11 | | cgzu 34107 |
. . . . . 6
class
AxUn |
12 | 3, 11, 6 | wbr 5109 |
. . . . 5
wff 𝑚⊧AxUn |
13 | | cgzg 34108 |
. . . . . 6
class
AxReg |
14 | 3, 13, 6 | wbr 5109 |
. . . . 5
wff 𝑚⊧AxReg |
15 | | cgzi 34109 |
. . . . . 6
class
AxInf |
16 | 3, 15, 6 | wbr 5109 |
. . . . 5
wff 𝑚⊧AxInf |
17 | 12, 14, 16 | w3a 1088 |
. . . 4
wff (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) |
18 | | vu |
. . . . . . . 8
setvar 𝑢 |
19 | 18 | cv 1541 |
. . . . . . 7
class 𝑢 |
20 | | cgzr 34105 |
. . . . . . 7
class
AxRep |
21 | 19, 20 | cfv 6500 |
. . . . . 6
class
(AxRep‘𝑢) |
22 | 3, 21, 6 | wbr 5109 |
. . . . 5
wff 𝑚⊧(AxRep‘𝑢) |
23 | | com 7806 |
. . . . . 6
class
ω |
24 | | cfmla 33995 |
. . . . . 6
class
Fmla |
25 | 23, 24 | cfv 6500 |
. . . . 5
class
(Fmla‘ω) |
26 | 22, 18, 25 | wral 3061 |
. . . 4
wff
∀𝑢 ∈
(Fmla‘ω)𝑚⊧(AxRep‘𝑢) |
27 | 10, 17, 26 | w3a 1088 |
. . 3
wff ((Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈
(Fmla‘ω)𝑚⊧(AxRep‘𝑢)) |
28 | 27, 2 | cab 2710 |
. 2
class {𝑚 ∣ ((Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈
(Fmla‘ω)𝑚⊧(AxRep‘𝑢))} |
29 | 1, 28 | wceq 1542 |
1
wff ZF = {𝑚 ∣ ((Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈
(Fmla‘ω)𝑚⊧(AxRep‘𝑢))} |