Detailed syntax breakdown of Axiom ax-iinf
Step | Hyp | Ref
| Expression |
1 | | c0 3394 |
. . . 4
class
∅ |
2 | | vx |
. . . . 5
setvar 𝑥 |
3 | 2 | cv 1334 |
. . . 4
class 𝑥 |
4 | 1, 3 | wcel 2128 |
. . 3
wff ∅
∈ 𝑥 |
5 | | vy |
. . . . . 6
setvar 𝑦 |
6 | 5, 2 | wel 2129 |
. . . . 5
wff 𝑦 ∈ 𝑥 |
7 | 5 | cv 1334 |
. . . . . . 7
class 𝑦 |
8 | 7 | csuc 4325 |
. . . . . 6
class suc 𝑦 |
9 | 8, 3 | wcel 2128 |
. . . . 5
wff suc 𝑦 ∈ 𝑥 |
10 | 6, 9 | wi 4 |
. . . 4
wff (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) |
11 | 10, 5 | wal 1333 |
. . 3
wff
∀𝑦(𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) |
12 | 4, 11 | wa 103 |
. 2
wff (∅
∈ 𝑥 ∧
∀𝑦(𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) |
13 | 12, 2 | wex 1472 |
1
wff
∃𝑥(∅
∈ 𝑥 ∧
∀𝑦(𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) |