Step | Hyp | Ref
| Expression |
1 | | eleq2 2098 |
. . . 4
⊢ (x = ∅ → (A ∈ x ↔ A ∈ ∅)) |
2 | | suceq 4105 |
. . . . 5
⊢ (x = ∅ → suc x = suc ∅) |
3 | 2 | eleq2d 2104 |
. . . 4
⊢ (x = ∅ → (suc A ∈ suc x ↔ suc A
∈ suc ∅)) |
4 | 1, 3 | imbi12d 223 |
. . 3
⊢ (x = ∅ → ((A ∈ x → suc A
∈ suc x)
↔ (A ∈ ∅ → suc A ∈ suc
∅))) |
5 | | eleq2 2098 |
. . . 4
⊢ (x = y →
(A ∈
x ↔ A ∈ y)) |
6 | | suceq 4105 |
. . . . 5
⊢ (x = y → suc
x = suc y) |
7 | 6 | eleq2d 2104 |
. . . 4
⊢ (x = y →
(suc A ∈
suc x ↔ suc A ∈ suc y)) |
8 | 5, 7 | imbi12d 223 |
. . 3
⊢ (x = y →
((A ∈
x → suc A ∈ suc x) ↔ (A
∈ y
→ suc A ∈ suc y))) |
9 | | eleq2 2098 |
. . . 4
⊢ (x = suc y →
(A ∈
x ↔ A ∈ suc y)) |
10 | | suceq 4105 |
. . . . 5
⊢ (x = suc y →
suc x = suc suc y) |
11 | 10 | eleq2d 2104 |
. . . 4
⊢ (x = suc y →
(suc A ∈
suc x ↔ suc A ∈ suc suc
y)) |
12 | 9, 11 | imbi12d 223 |
. . 3
⊢ (x = suc y →
((A ∈
x → suc A ∈ suc x) ↔ (A
∈ suc y
→ suc A ∈ suc suc y))) |
13 | | eleq2 2098 |
. . . 4
⊢ (x = B →
(A ∈
x ↔ A ∈ B)) |
14 | | suceq 4105 |
. . . . 5
⊢ (x = B → suc
x = suc B) |
15 | 14 | eleq2d 2104 |
. . . 4
⊢ (x = B →
(suc A ∈
suc x ↔ suc A ∈ suc B)) |
16 | 13, 15 | imbi12d 223 |
. . 3
⊢ (x = B →
((A ∈
x → suc A ∈ suc x) ↔ (A
∈ B
→ suc A ∈ suc B))) |
17 | | noel 3222 |
. . . 4
⊢ ¬
A ∈
∅ |
18 | 17 | pm2.21i 574 |
. . 3
⊢ (A ∈ ∅ →
suc A ∈
suc ∅) |
19 | | elsuci 4106 |
. . . . . . . 8
⊢ (A ∈ suc y → (A
∈ y ∨ A = y)) |
20 | 19 | adantl 262 |
. . . . . . 7
⊢
(((A ∈ y → suc
A ∈ suc
y) ∧
A ∈ suc
y) → (A ∈ y ∨ A = y)) |
21 | | simpl 102 |
. . . . . . . 8
⊢
(((A ∈ y → suc
A ∈ suc
y) ∧
A ∈ suc
y) → (A ∈ y → suc A
∈ suc y)) |
22 | | suceq 4105 |
. . . . . . . . 9
⊢ (A = y → suc
A = suc y) |
23 | 22 | a1i 9 |
. . . . . . . 8
⊢
(((A ∈ y → suc
A ∈ suc
y) ∧
A ∈ suc
y) → (A = y → suc
A = suc y)) |
24 | 21, 23 | orim12d 699 |
. . . . . . 7
⊢
(((A ∈ y → suc
A ∈ suc
y) ∧
A ∈ suc
y) → ((A ∈ y ∨ A = y) →
(suc A ∈
suc y ∨
suc A = suc y))) |
25 | 20, 24 | mpd 13 |
. . . . . 6
⊢
(((A ∈ y → suc
A ∈ suc
y) ∧
A ∈ suc
y) → (suc A ∈ suc y ∨ suc A = suc y)) |
26 | | vex 2554 |
. . . . . . . 8
⊢ y ∈
V |
27 | 26 | sucex 4191 |
. . . . . . 7
⊢ suc
y ∈
V |
28 | 27 | elsuc2 4110 |
. . . . . 6
⊢ (suc
A ∈ suc
suc y ↔ (suc A ∈ suc y ∨ suc A = suc y)) |
29 | 25, 28 | sylibr 137 |
. . . . 5
⊢
(((A ∈ y → suc
A ∈ suc
y) ∧
A ∈ suc
y) → suc A ∈ suc suc
y) |
30 | 29 | ex 108 |
. . . 4
⊢
((A ∈ y → suc
A ∈ suc
y) → (A ∈ suc y → suc A
∈ suc suc y)) |
31 | 30 | a1i 9 |
. . 3
⊢ (y ∈ 𝜔
→ ((A ∈ y → suc
A ∈ suc
y) → (A ∈ suc y → suc A
∈ suc suc y))) |
32 | 4, 8, 12, 16, 18, 31 | finds 4266 |
. 2
⊢ (B ∈ 𝜔
→ (A ∈ B → suc
A ∈ suc
B)) |
33 | | nnon 4275 |
. . 3
⊢ (B ∈ 𝜔
→ B ∈ On) |
34 | | onsucelsucr 4199 |
. . 3
⊢ (B ∈ On → (suc
A ∈ suc
B → A ∈ B)) |
35 | 33, 34 | syl 14 |
. 2
⊢ (B ∈ 𝜔
→ (suc A ∈ suc B →
A ∈
B)) |
36 | 32, 35 | impbid 120 |
1
⊢ (B ∈ 𝜔
→ (A ∈ B ↔ suc
A ∈ suc
B)) |