Detailed syntax breakdown of Axiom ax-sscoll
Step | Hyp | Ref
| Expression |
1 | | wph |
. . . . . . . 8
wff 𝜑 |
2 | | vy |
. . . . . . . 8
setvar 𝑦 |
3 | | vb |
. . . . . . . . 9
setvar 𝑏 |
4 | 3 | cv 1283 |
. . . . . . . 8
class 𝑏 |
5 | 1, 2, 4 | wrex 2349 |
. . . . . . 7
wff
∃𝑦 ∈
𝑏 𝜑 |
6 | | vx |
. . . . . . 7
setvar 𝑥 |
7 | | va |
. . . . . . . 8
setvar 𝑎 |
8 | 7 | cv 1283 |
. . . . . . 7
class 𝑎 |
9 | 5, 6, 8 | wral 2348 |
. . . . . 6
wff
∀𝑥 ∈
𝑎 ∃𝑦 ∈ 𝑏 𝜑 |
10 | | vd |
. . . . . . . . . 10
setvar 𝑑 |
11 | 2, 10 | wel 1434 |
. . . . . . . . 9
wff 𝑦 ∈ 𝑑 |
12 | 1, 6, 8 | wrex 2349 |
. . . . . . . . 9
wff
∃𝑥 ∈
𝑎 𝜑 |
13 | 11, 12 | wb 103 |
. . . . . . . 8
wff (𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑) |
14 | 13, 2 | wal 1282 |
. . . . . . 7
wff
∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑) |
15 | | vc |
. . . . . . . 8
setvar 𝑐 |
16 | 15 | cv 1283 |
. . . . . . 7
class 𝑐 |
17 | 14, 10, 16 | wrex 2349 |
. . . . . 6
wff
∃𝑑 ∈
𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑) |
18 | 9, 17 | wi 4 |
. . . . 5
wff
(∀𝑥 ∈
𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)) |
19 | | vz |
. . . . 5
setvar 𝑧 |
20 | 18, 19 | wal 1282 |
. . . 4
wff
∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)) |
21 | 20, 15 | wex 1421 |
. . 3
wff
∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)) |
22 | 21, 3 | wal 1282 |
. 2
wff
∀𝑏∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)) |
23 | 22, 7 | wal 1282 |
1
wff
∀𝑎∀𝑏∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)) |