Step | Hyp | Ref
| Expression |
1 | | ssexg 4804 |
. . . . . . . . 9
⊢ ((ω
⊆ 𝐵 ∧ 𝐵 ∈ On) → ω
∈ V) |
2 | 1 | ex 450 |
. . . . . . . 8
⊢ (ω
⊆ 𝐵 → (𝐵 ∈ On → ω ∈
V)) |
3 | | omelon2 7077 |
. . . . . . . 8
⊢ (ω
∈ V → ω ∈ On) |
4 | 2, 3 | syl6com 37 |
. . . . . . 7
⊢ (𝐵 ∈ On → (ω
⊆ 𝐵 → ω
∈ On)) |
5 | 4 | imp 445 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ ω ⊆
𝐵) → ω ∈
On) |
6 | 5 | adantll 750 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) → ω
∈ On) |
7 | | simplr 792 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) → 𝐵 ∈ On) |
8 | 6, 7 | jca 554 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) → (ω
∈ On ∧ 𝐵 ∈
On)) |
9 | | oawordeu 7635 |
. . . 4
⊢
(((ω ∈ On ∧ 𝐵 ∈ On) ∧ ω ⊆ 𝐵) → ∃!𝑥 ∈ On (ω
+𝑜 𝑥) =
𝐵) |
10 | 8, 9 | sylancom 701 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) →
∃!𝑥 ∈ On
(ω +𝑜 𝑥) = 𝐵) |
11 | | reurex 3160 |
. . 3
⊢
(∃!𝑥 ∈ On
(ω +𝑜 𝑥) = 𝐵 → ∃𝑥 ∈ On (ω +𝑜
𝑥) = 𝐵) |
12 | 10, 11 | syl 17 |
. 2
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) →
∃𝑥 ∈ On (ω
+𝑜 𝑥) =
𝐵) |
13 | | nnon 7071 |
. . . . . . 7
⊢ (𝐴 ∈ ω → 𝐴 ∈ On) |
14 | 13 | ad3antrrr 766 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝐴 ∈ On) |
15 | 6 | adantr 481 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) ∧ 𝑥 ∈ On) → ω
∈ On) |
16 | | simpr 477 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝑥 ∈ On) |
17 | | oaass 7641 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ ω ∈
On ∧ 𝑥 ∈ On)
→ ((𝐴
+𝑜 ω) +𝑜 𝑥) = (𝐴 +𝑜 (ω
+𝑜 𝑥))) |
18 | 14, 15, 16, 17 | syl3anc 1326 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +𝑜 ω)
+𝑜 𝑥) =
(𝐴 +𝑜
(ω +𝑜 𝑥))) |
19 | | simpll 790 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) → 𝐴 ∈
ω) |
20 | | oaabslem 7723 |
. . . . . . . 8
⊢ ((ω
∈ On ∧ 𝐴 ∈
ω) → (𝐴
+𝑜 ω) = ω) |
21 | 6, 19, 20 | syl2anc 693 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) → (𝐴 +𝑜 ω)
= ω) |
22 | 21 | adantr 481 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +𝑜 ω)
= ω) |
23 | 22 | oveq1d 6665 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +𝑜 ω)
+𝑜 𝑥) =
(ω +𝑜 𝑥)) |
24 | 18, 23 | eqtr3d 2658 |
. . . 4
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +𝑜 (ω
+𝑜 𝑥)) =
(ω +𝑜 𝑥)) |
25 | | oveq2 6658 |
. . . . 5
⊢ ((ω
+𝑜 𝑥) =
𝐵 → (𝐴 +𝑜 (ω
+𝑜 𝑥)) =
(𝐴 +𝑜
𝐵)) |
26 | | id 22 |
. . . . 5
⊢ ((ω
+𝑜 𝑥) =
𝐵 → (ω
+𝑜 𝑥) =
𝐵) |
27 | 25, 26 | eqeq12d 2637 |
. . . 4
⊢ ((ω
+𝑜 𝑥) =
𝐵 → ((𝐴 +𝑜 (ω
+𝑜 𝑥)) =
(ω +𝑜 𝑥) ↔ (𝐴 +𝑜 𝐵) = 𝐵)) |
28 | 24, 27 | syl5ibcom 235 |
. . 3
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) ∧ 𝑥 ∈ On) → ((ω
+𝑜 𝑥) =
𝐵 → (𝐴 +𝑜 𝐵) = 𝐵)) |
29 | 28 | rexlimdva 3031 |
. 2
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) →
(∃𝑥 ∈ On
(ω +𝑜 𝑥) = 𝐵 → (𝐴 +𝑜 𝐵) = 𝐵)) |
30 | 12, 29 | mpd 15 |
1
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω
⊆ 𝐵) → (𝐴 +𝑜 𝐵) = 𝐵) |