Step | Hyp | Ref
| Expression |
1 | | eloni 4078 |
. . . . . . . 8
⊢ (𝑏 ∈ On → Ord 𝑏) |
2 | | ordtr 4081 |
. . . . . . . 8
⊢ (Ord
𝑏 → Tr 𝑏) |
3 | 1, 2 | syl 14 |
. . . . . . 7
⊢ (𝑏 ∈ On → Tr 𝑏) |
4 | | vex 2554 |
. . . . . . . 8
⊢ 𝑏 ∈ V |
5 | 4 | unisuc 4116 |
. . . . . . 7
⊢ (Tr 𝑏 ↔ ∪ suc 𝑏 =
𝑏) |
6 | 3, 5 | sylib 127 |
. . . . . 6
⊢ (𝑏 ∈ On → ∪ suc 𝑏 = 𝑏) |
7 | 6 | eleq2d 2104 |
. . . . 5
⊢ (𝑏 ∈ On → (𝑎 ∈ ∪ suc 𝑏
↔ 𝑎 ∈ 𝑏)) |
8 | 7 | adantl 262 |
. . . 4
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 ∈ ∪ suc 𝑏
↔ 𝑎 ∈ 𝑏)) |
9 | | suceloni 4193 |
. . . . 5
⊢ (𝑏 ∈ On → suc 𝑏 ∈
On) |
10 | | ordsucunielexmid.1 |
. . . . . 6
⊢ ∀x ∈ On ∀y ∈ On (x ∈ ∪ y → suc
x ∈
y) |
11 | | eleq1 2097 |
. . . . . . . 8
⊢ (x = 𝑎 → (x ∈ ∪ y ↔ 𝑎 ∈ ∪ y)) |
12 | | suceq 4105 |
. . . . . . . . 9
⊢ (x = 𝑎 → suc x = suc 𝑎) |
13 | 12 | eleq1d 2103 |
. . . . . . . 8
⊢ (x = 𝑎 → (suc x ∈ y ↔ suc 𝑎 ∈ y)) |
14 | 11, 13 | imbi12d 223 |
. . . . . . 7
⊢ (x = 𝑎 → ((x ∈ ∪ y → suc
x ∈
y) ↔ (𝑎 ∈ ∪ y → suc 𝑎 ∈ y))) |
15 | | unieq 3580 |
. . . . . . . . 9
⊢ (y = suc 𝑏 → ∪ y = ∪ suc 𝑏) |
16 | 15 | eleq2d 2104 |
. . . . . . . 8
⊢ (y = suc 𝑏 → (𝑎 ∈ ∪ y ↔ 𝑎 ∈ ∪ suc 𝑏)) |
17 | | eleq2 2098 |
. . . . . . . 8
⊢ (y = suc 𝑏 → (suc 𝑎 ∈ y ↔ suc 𝑎 ∈ suc
𝑏)) |
18 | 16, 17 | imbi12d 223 |
. . . . . . 7
⊢ (y = suc 𝑏 → ((𝑎 ∈ ∪ y → suc 𝑎 ∈ y) ↔
(𝑎 ∈ ∪ suc 𝑏 → suc 𝑎 ∈ suc
𝑏))) |
19 | 14, 18 | rspc2va 2657 |
. . . . . 6
⊢ (((𝑎 ∈ On ∧ suc 𝑏 ∈ On) ∧ ∀x ∈ On ∀y ∈ On (x ∈ ∪ y → suc
x ∈
y)) → (𝑎 ∈ ∪ suc 𝑏
→ suc 𝑎 ∈ suc 𝑏)) |
20 | 10, 19 | mpan2 401 |
. . . . 5
⊢ ((𝑎 ∈ On ∧ suc 𝑏 ∈ On) → (𝑎 ∈ ∪ suc 𝑏
→ suc 𝑎 ∈ suc 𝑏)) |
21 | 9, 20 | sylan2 270 |
. . . 4
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 ∈ ∪ suc 𝑏
→ suc 𝑎 ∈ suc 𝑏)) |
22 | 8, 21 | sylbird 159 |
. . 3
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 ∈ 𝑏 → suc 𝑎 ∈ suc
𝑏)) |
23 | 22 | rgen2a 2369 |
. 2
⊢ ∀𝑎 ∈ On ∀𝑏 ∈ On
(𝑎 ∈ 𝑏 → suc 𝑎 ∈ suc
𝑏) |
24 | 23 | onsucelsucexmid 4215 |
1
⊢ (φ ∨ ¬
φ) |