Step | Hyp | Ref
| Expression |
1 | | eqeq1 2043 |
. . 3
⊢ (y = ∅ → (y = ∅ ↔ ∅ =
∅)) |
2 | | eqeq1 2043 |
. . . 4
⊢ (y = ∅ → (y = suc x ↔
∅ = suc x)) |
3 | 2 | rexbidv 2321 |
. . 3
⊢ (y = ∅ → (∃x ∈ 𝜔 y =
suc x ↔ ∃x ∈ 𝜔 ∅ = suc x)) |
4 | 1, 3 | orbi12d 706 |
. 2
⊢ (y = ∅ → ((y = ∅ ∨ ∃x ∈ 𝜔 y =
suc x) ↔ (∅ = ∅ ∨ ∃x ∈ 𝜔
∅ = suc x))) |
5 | | eqeq1 2043 |
. . 3
⊢ (y = z →
(y = ∅ ↔ z = ∅)) |
6 | | eqeq1 2043 |
. . . 4
⊢ (y = z →
(y = suc x ↔ z = suc
x)) |
7 | 6 | rexbidv 2321 |
. . 3
⊢ (y = z →
(∃x
∈ 𝜔 y = suc x ↔
∃x ∈ 𝜔 z =
suc x)) |
8 | 5, 7 | orbi12d 706 |
. 2
⊢ (y = z →
((y = ∅
∨ ∃x ∈ 𝜔
y = suc x) ↔ (z =
∅ ∨ ∃x ∈ 𝜔 z =
suc x))) |
9 | | eqeq1 2043 |
. . 3
⊢ (y = suc z →
(y = ∅ ↔ suc z = ∅)) |
10 | | eqeq1 2043 |
. . . 4
⊢ (y = suc z →
(y = suc x ↔ suc z =
suc x)) |
11 | 10 | rexbidv 2321 |
. . 3
⊢ (y = suc z →
(∃x
∈ 𝜔 y = suc x ↔
∃x ∈ 𝜔 suc z = suc x)) |
12 | 9, 11 | orbi12d 706 |
. 2
⊢ (y = suc z →
((y = ∅
∨ ∃x ∈ 𝜔
y = suc x) ↔ (suc z
= ∅ ∨ ∃x ∈ 𝜔 suc z = suc x))) |
13 | | eqeq1 2043 |
. . 3
⊢ (y = A →
(y = ∅ ↔ A = ∅)) |
14 | | eqeq1 2043 |
. . . 4
⊢ (y = A →
(y = suc x ↔ A = suc
x)) |
15 | 14 | rexbidv 2321 |
. . 3
⊢ (y = A →
(∃x
∈ 𝜔 y = suc x ↔
∃x ∈ 𝜔 A =
suc x)) |
16 | 13, 15 | orbi12d 706 |
. 2
⊢ (y = A →
((y = ∅
∨ ∃x ∈ 𝜔
y = suc x) ↔ (A =
∅ ∨ ∃x ∈ 𝜔 A =
suc x))) |
17 | | eqid 2037 |
. . 3
⊢ ∅ =
∅ |
18 | 17 | orci 649 |
. 2
⊢ (∅
= ∅ ∨ ∃x ∈ 𝜔 ∅ = suc x) |
19 | | eqid 2037 |
. . . . 5
⊢ suc
z = suc z |
20 | | suceq 4105 |
. . . . . . 7
⊢ (x = z → suc
x = suc z) |
21 | 20 | eqeq2d 2048 |
. . . . . 6
⊢ (x = z →
(suc z = suc x ↔ suc z =
suc z)) |
22 | 21 | rspcev 2650 |
. . . . 5
⊢
((z ∈ 𝜔 ∧ suc
z = suc z) → ∃x ∈ 𝜔 suc z = suc x) |
23 | 19, 22 | mpan2 401 |
. . . 4
⊢ (z ∈ 𝜔
→ ∃x ∈ 𝜔 suc
z = suc x) |
24 | 23 | olcd 652 |
. . 3
⊢ (z ∈ 𝜔
→ (suc z = ∅ ∨ ∃x ∈ 𝜔 suc
z = suc x)) |
25 | 24 | a1d 22 |
. 2
⊢ (z ∈ 𝜔
→ ((z = ∅
∨ ∃x ∈ 𝜔
z = suc x) → (suc z
= ∅ ∨ ∃x ∈ 𝜔 suc z = suc x))) |
26 | 4, 8, 12, 16, 18, 25 | finds 4266 |
1
⊢ (A ∈ 𝜔
→ (A = ∅
∨ ∃x ∈ 𝜔
A = suc x)) |