Step | Hyp | Ref
| Expression |
1 | | eqeq1 2043 |
. . 3
⊢ (x = ∅ → (x = ∅ ↔ ∅ =
∅)) |
2 | | eleq2 2098 |
. . 3
⊢ (x = ∅ → (∅ ∈ x ↔
∅ ∈ ∅)) |
3 | 1, 2 | orbi12d 706 |
. 2
⊢ (x = ∅ → ((x = ∅ ∨
∅ ∈ x) ↔ (∅ = ∅
∨ ∅ ∈
∅))) |
4 | | eqeq1 2043 |
. . 3
⊢ (x = y →
(x = ∅ ↔ y = ∅)) |
5 | | eleq2 2098 |
. . 3
⊢ (x = y →
(∅ ∈ x ↔ ∅ ∈
y)) |
6 | 4, 5 | orbi12d 706 |
. 2
⊢ (x = y →
((x = ∅
∨ ∅ ∈ x) ↔ (y =
∅ ∨ ∅ ∈ y))) |
7 | | eqeq1 2043 |
. . 3
⊢ (x = suc y →
(x = ∅ ↔ suc y = ∅)) |
8 | | eleq2 2098 |
. . 3
⊢ (x = suc y →
(∅ ∈ x ↔ ∅ ∈
suc y)) |
9 | 7, 8 | orbi12d 706 |
. 2
⊢ (x = suc y →
((x = ∅
∨ ∅ ∈ x) ↔ (suc y
= ∅ ∨ ∅ ∈ suc y))) |
10 | | eqeq1 2043 |
. . 3
⊢ (x = A →
(x = ∅ ↔ A = ∅)) |
11 | | eleq2 2098 |
. . 3
⊢ (x = A →
(∅ ∈ x ↔ ∅ ∈
A)) |
12 | 10, 11 | orbi12d 706 |
. 2
⊢ (x = A →
((x = ∅
∨ ∅ ∈ x) ↔ (A =
∅ ∨ ∅ ∈ A))) |
13 | | eqid 2037 |
. . 3
⊢ ∅ =
∅ |
14 | 13 | orci 649 |
. 2
⊢ (∅
= ∅ ∨ ∅ ∈ ∅) |
15 | | 0ex 3875 |
. . . . . . 7
⊢ ∅
∈ V |
16 | 15 | sucid 4120 |
. . . . . 6
⊢ ∅
∈ suc ∅ |
17 | | suceq 4105 |
. . . . . 6
⊢ (y = ∅ → suc y = suc ∅) |
18 | 16, 17 | syl5eleqr 2124 |
. . . . 5
⊢ (y = ∅ → ∅ ∈ suc y) |
19 | 18 | a1i 9 |
. . . 4
⊢ (y ∈ 𝜔
→ (y = ∅ → ∅ ∈ suc y)) |
20 | | sssucid 4118 |
. . . . . 6
⊢ y ⊆ suc y |
21 | 20 | a1i 9 |
. . . . 5
⊢ (y ∈ 𝜔
→ y ⊆ suc y) |
22 | 21 | sseld 2938 |
. . . 4
⊢ (y ∈ 𝜔
→ (∅ ∈ y → ∅ ∈
suc y)) |
23 | 19, 22 | jaod 636 |
. . 3
⊢ (y ∈ 𝜔
→ ((y = ∅
∨ ∅ ∈ y) → ∅ ∈ suc y)) |
24 | | olc 631 |
. . 3
⊢ (∅
∈ suc y
→ (suc y = ∅ ∨ ∅ ∈ suc
y)) |
25 | 23, 24 | syl6 29 |
. 2
⊢ (y ∈ 𝜔
→ ((y = ∅
∨ ∅ ∈ y) → (suc y
= ∅ ∨ ∅ ∈ suc y))) |
26 | 3, 6, 9, 12, 14, 25 | finds 4266 |
1
⊢ (A ∈ 𝜔
→ (A = ∅
∨ ∅ ∈ A)) |