Step | Hyp | Ref
| Expression |
1 | | ssexg 5216 |
. . . . . . . . 9
⊢ ((ω
⊆ 𝐵 ∧ 𝐵 ∈ On) → ω
∈ V) |
2 | 1 | ex 416 |
. . . . . . . 8
⊢ (ω
⊆ 𝐵 → (𝐵 ∈ On → ω ∈
V)) |
3 | | omelon2 7657 |
. . . . . . . 8
⊢ (ω
∈ V → ω ∈ On) |
4 | 2, 3 | syl6com 37 |
. . . . . . 7
⊢ (𝐵 ∈ On → (ω
⊆ 𝐵 → ω
∈ On)) |
5 | 4 | imp 410 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ ω ⊆
𝐵) → ω ∈
On) |
6 | 5 | adantll 714 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) → ω
∈ On) |
7 | | simplr 769 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) → 𝐵 ∈ On) |
8 | 6, 7 | jca 515 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) → (ω
∈ On ∧ 𝐵 ∈
On)) |
9 | | oawordeu 8283 |
. . . 4
⊢
(((ω ∈ On ∧ 𝐵 ∈ On) ∧ ω ⊆ 𝐵) → ∃!𝑥 ∈ On (ω
+o 𝑥) = 𝐵) |
10 | 8, 9 | sylancom 591 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) →
∃!𝑥 ∈ On
(ω +o 𝑥) =
𝐵) |
11 | | reurex 3338 |
. . 3
⊢
(∃!𝑥 ∈ On
(ω +o 𝑥) =
𝐵 → ∃𝑥 ∈ On (ω
+o 𝑥) = 𝐵) |
12 | 10, 11 | syl 17 |
. 2
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) →
∃𝑥 ∈ On (ω
+o 𝑥) = 𝐵) |
13 | | nnon 7650 |
. . . . . . 7
⊢ (𝐴 ∈ ω → 𝐴 ∈ On) |
14 | 13 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝐴 ∈ On) |
15 | 6 | adantr 484 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) ∧ 𝑥 ∈ On) → ω
∈ On) |
16 | | simpr 488 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝑥 ∈ On) |
17 | | oaass 8289 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ ω ∈
On ∧ 𝑥 ∈ On)
→ ((𝐴 +o
ω) +o 𝑥) =
(𝐴 +o (ω
+o 𝑥))) |
18 | 14, 15, 16, 17 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +o ω)
+o 𝑥) = (𝐴 +o (ω
+o 𝑥))) |
19 | | simpll 767 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) → 𝐴 ∈
ω) |
20 | | oaabslem 8372 |
. . . . . . . 8
⊢ ((ω
∈ On ∧ 𝐴 ∈
ω) → (𝐴
+o ω) = ω) |
21 | 6, 19, 20 | syl2anc 587 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) → (𝐴 +o ω) =
ω) |
22 | 21 | adantr 484 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +o ω) =
ω) |
23 | 22 | oveq1d 7228 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +o ω)
+o 𝑥) = (ω
+o 𝑥)) |
24 | 18, 23 | eqtr3d 2779 |
. . . 4
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +o (ω
+o 𝑥)) =
(ω +o 𝑥)) |
25 | | oveq2 7221 |
. . . . 5
⊢ ((ω
+o 𝑥) = 𝐵 → (𝐴 +o (ω +o 𝑥)) = (𝐴 +o 𝐵)) |
26 | | id 22 |
. . . . 5
⊢ ((ω
+o 𝑥) = 𝐵 → (ω +o
𝑥) = 𝐵) |
27 | 25, 26 | eqeq12d 2753 |
. . . 4
⊢ ((ω
+o 𝑥) = 𝐵 → ((𝐴 +o (ω +o 𝑥)) = (ω +o
𝑥) ↔ (𝐴 +o 𝐵) = 𝐵)) |
28 | 24, 27 | syl5ibcom 248 |
. . 3
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) ∧ 𝑥 ∈ On) → ((ω
+o 𝑥) = 𝐵 → (𝐴 +o 𝐵) = 𝐵)) |
29 | 28 | rexlimdva 3203 |
. 2
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) →
(∃𝑥 ∈ On
(ω +o 𝑥) =
𝐵 → (𝐴 +o 𝐵) = 𝐵)) |
30 | 12, 29 | mpd 15 |
1
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) → (𝐴 +o 𝐵) = 𝐵) |