Detailed syntax breakdown of Axiom ax-groth
Step | Hyp | Ref
| Expression |
1 | | vx |
. . . 4
setvar 𝑥 |
2 | | vy |
. . . 4
setvar 𝑦 |
3 | 1, 2 | wel 2108 |
. . 3
wff 𝑥 ∈ 𝑦 |
4 | | vw |
. . . . . . . . 9
setvar 𝑤 |
5 | 4 | cv 1538 |
. . . . . . . 8
class 𝑤 |
6 | | vz |
. . . . . . . . 9
setvar 𝑧 |
7 | 6 | cv 1538 |
. . . . . . . 8
class 𝑧 |
8 | 5, 7 | wss 3888 |
. . . . . . 7
wff 𝑤 ⊆ 𝑧 |
9 | 4, 2 | wel 2108 |
. . . . . . 7
wff 𝑤 ∈ 𝑦 |
10 | 8, 9 | wi 4 |
. . . . . 6
wff (𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) |
11 | 10, 4 | wal 1537 |
. . . . 5
wff
∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) |
12 | | vv |
. . . . . . . . . 10
setvar 𝑣 |
13 | 12 | cv 1538 |
. . . . . . . . 9
class 𝑣 |
14 | 13, 7 | wss 3888 |
. . . . . . . 8
wff 𝑣 ⊆ 𝑧 |
15 | 12, 4 | wel 2108 |
. . . . . . . 8
wff 𝑣 ∈ 𝑤 |
16 | 14, 15 | wi 4 |
. . . . . . 7
wff (𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤) |
17 | 16, 12 | wal 1537 |
. . . . . 6
wff
∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤) |
18 | 2 | cv 1538 |
. . . . . 6
class 𝑦 |
19 | 17, 4, 18 | wrex 3063 |
. . . . 5
wff
∃𝑤 ∈
𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤) |
20 | 11, 19 | wa 395 |
. . . 4
wff
(∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) |
21 | 20, 6, 18 | wral 3062 |
. . 3
wff
∀𝑧 ∈
𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) |
22 | 7, 18 | wss 3888 |
. . . . 5
wff 𝑧 ⊆ 𝑦 |
23 | | cen 8693 |
. . . . . . 7
class
≈ |
24 | 7, 18, 23 | wbr 5075 |
. . . . . 6
wff 𝑧 ≈ 𝑦 |
25 | 6, 2 | wel 2108 |
. . . . . 6
wff 𝑧 ∈ 𝑦 |
26 | 24, 25 | wo 843 |
. . . . 5
wff (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦) |
27 | 22, 26 | wi 4 |
. . . 4
wff (𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)) |
28 | 27, 6 | wal 1537 |
. . 3
wff
∀𝑧(𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)) |
29 | 3, 21, 28 | w3a 1085 |
. 2
wff (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))) |
30 | 29, 2 | wex 1783 |
1
wff
∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))) |