Step | Hyp | Ref
| Expression |
1 | | eqeq1 2171 |
. . 3
⊢ (𝑦 = ∅ → (𝑦 = ∅ ↔ ∅ =
∅)) |
2 | | eqeq1 2171 |
. . . 4
⊢ (𝑦 = ∅ → (𝑦 = suc 𝑥 ↔ ∅ = suc 𝑥)) |
3 | 2 | rexbidv 2465 |
. . 3
⊢ (𝑦 = ∅ → (∃𝑥 ∈ ω 𝑦 = suc 𝑥 ↔ ∃𝑥 ∈ ω ∅ = suc 𝑥)) |
4 | 1, 3 | orbi12d 783 |
. 2
⊢ (𝑦 = ∅ → ((𝑦 = ∅ ∨ ∃𝑥 ∈ ω 𝑦 = suc 𝑥) ↔ (∅ = ∅ ∨ ∃𝑥 ∈ ω ∅ = suc
𝑥))) |
5 | | eqeq1 2171 |
. . 3
⊢ (𝑦 = 𝑧 → (𝑦 = ∅ ↔ 𝑧 = ∅)) |
6 | | eqeq1 2171 |
. . . 4
⊢ (𝑦 = 𝑧 → (𝑦 = suc 𝑥 ↔ 𝑧 = suc 𝑥)) |
7 | 6 | rexbidv 2465 |
. . 3
⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ ω 𝑦 = suc 𝑥 ↔ ∃𝑥 ∈ ω 𝑧 = suc 𝑥)) |
8 | 5, 7 | orbi12d 783 |
. 2
⊢ (𝑦 = 𝑧 → ((𝑦 = ∅ ∨ ∃𝑥 ∈ ω 𝑦 = suc 𝑥) ↔ (𝑧 = ∅ ∨ ∃𝑥 ∈ ω 𝑧 = suc 𝑥))) |
9 | | eqeq1 2171 |
. . 3
⊢ (𝑦 = suc 𝑧 → (𝑦 = ∅ ↔ suc 𝑧 = ∅)) |
10 | | eqeq1 2171 |
. . . 4
⊢ (𝑦 = suc 𝑧 → (𝑦 = suc 𝑥 ↔ suc 𝑧 = suc 𝑥)) |
11 | 10 | rexbidv 2465 |
. . 3
⊢ (𝑦 = suc 𝑧 → (∃𝑥 ∈ ω 𝑦 = suc 𝑥 ↔ ∃𝑥 ∈ ω suc 𝑧 = suc 𝑥)) |
12 | 9, 11 | orbi12d 783 |
. 2
⊢ (𝑦 = suc 𝑧 → ((𝑦 = ∅ ∨ ∃𝑥 ∈ ω 𝑦 = suc 𝑥) ↔ (suc 𝑧 = ∅ ∨ ∃𝑥 ∈ ω suc 𝑧 = suc 𝑥))) |
13 | | eqeq1 2171 |
. . 3
⊢ (𝑦 = 𝐴 → (𝑦 = ∅ ↔ 𝐴 = ∅)) |
14 | | eqeq1 2171 |
. . . 4
⊢ (𝑦 = 𝐴 → (𝑦 = suc 𝑥 ↔ 𝐴 = suc 𝑥)) |
15 | 14 | rexbidv 2465 |
. . 3
⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ ω 𝑦 = suc 𝑥 ↔ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) |
16 | 13, 15 | orbi12d 783 |
. 2
⊢ (𝑦 = 𝐴 → ((𝑦 = ∅ ∨ ∃𝑥 ∈ ω 𝑦 = suc 𝑥) ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥))) |
17 | | eqid 2164 |
. . 3
⊢ ∅ =
∅ |
18 | 17 | orci 721 |
. 2
⊢ (∅
= ∅ ∨ ∃𝑥
∈ ω ∅ = suc 𝑥) |
19 | | eqid 2164 |
. . . . 5
⊢ suc 𝑧 = suc 𝑧 |
20 | | suceq 4377 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧) |
21 | 20 | eqeq2d 2176 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (suc 𝑧 = suc 𝑥 ↔ suc 𝑧 = suc 𝑧)) |
22 | 21 | rspcev 2828 |
. . . . 5
⊢ ((𝑧 ∈ ω ∧ suc 𝑧 = suc 𝑧) → ∃𝑥 ∈ ω suc 𝑧 = suc 𝑥) |
23 | 19, 22 | mpan2 422 |
. . . 4
⊢ (𝑧 ∈ ω →
∃𝑥 ∈ ω suc
𝑧 = suc 𝑥) |
24 | 23 | olcd 724 |
. . 3
⊢ (𝑧 ∈ ω → (suc
𝑧 = ∅ ∨
∃𝑥 ∈ ω suc
𝑧 = suc 𝑥)) |
25 | 24 | a1d 22 |
. 2
⊢ (𝑧 ∈ ω → ((𝑧 = ∅ ∨ ∃𝑥 ∈ ω 𝑧 = suc 𝑥) → (suc 𝑧 = ∅ ∨ ∃𝑥 ∈ ω suc 𝑧 = suc 𝑥))) |
26 | 4, 8, 12, 16, 18, 25 | finds 4574 |
1
⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) |