Step | Hyp | Ref
| Expression |
1 | | n0i 3879 |
. . . . . . 7
⊢ (𝐴 ∈ (ω
↑𝑜 𝐶) → ¬ (ω
↑𝑜 𝐶) = ∅) |
2 | | fnoe 7477 |
. . . . . . . . 9
⊢
↑𝑜 Fn (On × On) |
3 | | fndm 5904 |
. . . . . . . . 9
⊢ (
↑𝑜 Fn (On × On) → dom
↑𝑜 = (On × On)) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . 8
⊢ dom
↑𝑜 = (On × On) |
5 | 4 | ndmov 6716 |
. . . . . . 7
⊢ (¬
(ω ∈ On ∧ 𝐶
∈ On) → (ω ↑𝑜 𝐶) = ∅) |
6 | 1, 5 | nsyl2 141 |
. . . . . 6
⊢ (𝐴 ∈ (ω
↑𝑜 𝐶) → (ω ∈ On ∧ 𝐶 ∈ On)) |
7 | 6 | ad2antrr 758 |
. . . . 5
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → (ω ∈ On ∧ 𝐶 ∈ On)) |
8 | | oecl 7504 |
. . . . 5
⊢ ((ω
∈ On ∧ 𝐶 ∈
On) → (ω ↑𝑜 𝐶) ∈ On) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜
𝐶) ∈
On) |
10 | | simplr 788 |
. . . 4
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → 𝐵 ∈ On) |
11 | | simpr 476 |
. . . 4
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜
𝐶) ⊆ 𝐵) |
12 | | oawordeu 7522 |
. . . 4
⊢
((((ω ↑𝑜 𝐶) ∈ On ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → ∃!𝑥 ∈ On ((ω
↑𝑜 𝐶) +𝑜 𝑥) = 𝐵) |
13 | 9, 10, 11, 12 | syl21anc 1317 |
. . 3
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → ∃!𝑥 ∈ On ((ω
↑𝑜 𝐶) +𝑜 𝑥) = 𝐵) |
14 | | reurex 3137 |
. . 3
⊢
(∃!𝑥 ∈ On
((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → ∃𝑥 ∈ On ((ω
↑𝑜 𝐶) +𝑜 𝑥) = 𝐵) |
15 | 13, 14 | syl 17 |
. 2
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → ∃𝑥 ∈ On ((ω
↑𝑜 𝐶) +𝑜 𝑥) = 𝐵) |
16 | | simpll 786 |
. . . . . . . 8
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → 𝐴 ∈ (ω ↑𝑜
𝐶)) |
17 | | onelon 5665 |
. . . . . . . 8
⊢
(((ω ↑𝑜 𝐶) ∈ On ∧ 𝐴 ∈ (ω ↑𝑜
𝐶)) → 𝐴 ∈ On) |
18 | 9, 16, 17 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → 𝐴 ∈ On) |
19 | 18 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝐴 ∈ On) |
20 | 9 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (ω
↑𝑜 𝐶) ∈ On) |
21 | | simpr 476 |
. . . . . 6
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝑥 ∈ On) |
22 | | oaass 7528 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ (ω
↑𝑜 𝐶) ∈ On ∧ 𝑥 ∈ On) → ((𝐴 +𝑜 (ω
↑𝑜 𝐶)) +𝑜 𝑥) = (𝐴 +𝑜 ((ω
↑𝑜 𝐶) +𝑜 𝑥))) |
23 | 19, 20, 21, 22 | syl3anc 1318 |
. . . . 5
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +𝑜 (ω
↑𝑜 𝐶)) +𝑜 𝑥) = (𝐴 +𝑜 ((ω
↑𝑜 𝐶) +𝑜 𝑥))) |
24 | 7 | simprd 478 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → 𝐶 ∈ On) |
25 | | eloni 5650 |
. . . . . . . . . 10
⊢ (𝐶 ∈ On → Ord 𝐶) |
26 | 24, 25 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → Ord 𝐶) |
27 | | ordzsl 6937 |
. . . . . . . . 9
⊢ (Ord
𝐶 ↔ (𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶)) |
28 | 26, 27 | sylib 207 |
. . . . . . . 8
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → (𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶)) |
29 | | simplll 794 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 ∈ (ω ↑𝑜
𝐶)) |
30 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 = ∅ → (ω
↑𝑜 𝐶) = (ω ↑𝑜
∅)) |
31 | 7 | simpld 474 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → ω ∈ On) |
32 | | oe0 7489 |
. . . . . . . . . . . . . . . 16
⊢ (ω
∈ On → (ω ↑𝑜 ∅) =
1𝑜) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜
∅) = 1𝑜) |
34 | 30, 33 | sylan9eqr 2666 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (ω
↑𝑜 𝐶) = 1𝑜) |
35 | 29, 34 | eleqtrd 2690 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 ∈
1𝑜) |
36 | | el1o 7466 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 1𝑜
↔ 𝐴 =
∅) |
37 | 35, 36 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 = ∅) |
38 | 37 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) = (∅ +𝑜 (ω
↑𝑜 𝐶))) |
39 | 9 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (ω
↑𝑜 𝐶) ∈ On) |
40 | | oa0r 7505 |
. . . . . . . . . . . 12
⊢ ((ω
↑𝑜 𝐶) ∈ On → (∅
+𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜
𝐶)) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (∅
+𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜
𝐶)) |
42 | 38, 41 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) = (ω ↑𝑜
𝐶)) |
43 | 42 | ex 449 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → (𝐶 = ∅ → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) = (ω ↑𝑜
𝐶))) |
44 | 31 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → ω ∈ On) |
45 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝑥 ∈ On) |
46 | | oecl 7504 |
. . . . . . . . . . . . . 14
⊢ ((ω
∈ On ∧ 𝑥 ∈
On) → (ω ↑𝑜 𝑥) ∈ On) |
47 | 44, 45, 46 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜
𝑥) ∈
On) |
48 | | limom 6972 |
. . . . . . . . . . . . . 14
⊢ Lim
ω |
49 | 44, 48 | jctir 559 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ∈ On ∧ Lim
ω)) |
50 | | simplll 794 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐴 ∈ (ω ↑𝑜
𝐶)) |
51 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐶 = suc 𝑥) |
52 | 51 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜
𝐶) = (ω
↑𝑜 suc 𝑥)) |
53 | | oesuc 7494 |
. . . . . . . . . . . . . . . 16
⊢ ((ω
∈ On ∧ 𝑥 ∈
On) → (ω ↑𝑜 suc 𝑥) = ((ω ↑𝑜
𝑥)
·𝑜 ω)) |
54 | 44, 45, 53 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜
suc 𝑥) = ((ω
↑𝑜 𝑥) ·𝑜
ω)) |
55 | 52, 54 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜
𝐶) = ((ω
↑𝑜 𝑥) ·𝑜
ω)) |
56 | 50, 55 | eleqtrd 2690 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 ω)) |
57 | | omordlim 7544 |
. . . . . . . . . . . . 13
⊢
((((ω ↑𝑜 𝑥) ∈ On ∧ (ω ∈ On ∧
Lim ω)) ∧ 𝐴
∈ ((ω ↑𝑜 𝑥) ·𝑜 ω))
→ ∃𝑦 ∈
ω 𝐴 ∈ ((ω
↑𝑜 𝑥) ·𝑜 𝑦)) |
58 | 47, 49, 56, 57 | syl21anc 1317 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → ∃𝑦 ∈ ω 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦)) |
59 | 47 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → (ω
↑𝑜 𝑥) ∈ On) |
60 | | nnon 6963 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ω → 𝑦 ∈ On) |
61 | 60 | ad2antrl 760 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → 𝑦 ∈ On) |
62 | | omcl 7503 |
. . . . . . . . . . . . . . . . 17
⊢
(((ω ↑𝑜 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω
↑𝑜 𝑥) ·𝑜 𝑦) ∈ On) |
63 | 59, 61, 62 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → ((ω
↑𝑜 𝑥) ·𝑜 𝑦) ∈ On) |
64 | | eloni 5650 |
. . . . . . . . . . . . . . . 16
⊢
(((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∈ On → Ord ((ω
↑𝑜 𝑥) ·𝑜 𝑦)) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → Ord ((ω
↑𝑜 𝑥) ·𝑜 𝑦)) |
66 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦)) |
67 | | ordelss 5656 |
. . . . . . . . . . . . . . 15
⊢ ((Ord
((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦)) → 𝐴 ⊆ ((ω
↑𝑜 𝑥) ·𝑜 𝑦)) |
68 | 65, 66, 67 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → 𝐴 ⊆ ((ω
↑𝑜 𝑥) ·𝑜 𝑦)) |
69 | 18 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → 𝐴 ∈ On) |
70 | 9 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → (ω
↑𝑜 𝐶) ∈ On) |
71 | | oawordri 7517 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ On ∧ ((ω
↑𝑜 𝑥) ·𝑜 𝑦) ∈ On ∧ (ω
↑𝑜 𝐶) ∈ On) → (𝐴 ⊆ ((ω
↑𝑜 𝑥) ·𝑜 𝑦) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) ⊆ (((ω
↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω
↑𝑜 𝐶)))) |
72 | 69, 63, 70, 71 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → (𝐴 ⊆ ((ω
↑𝑜 𝑥) ·𝑜 𝑦) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) ⊆ (((ω
↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω
↑𝑜 𝐶)))) |
73 | 68, 72 | mpd 15 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) ⊆ (((ω
↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω
↑𝑜 𝐶))) |
74 | 44 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → ω ∈
On) |
75 | | odi 7546 |
. . . . . . . . . . . . . . . 16
⊢
(((ω ↑𝑜 𝑥) ∈ On ∧ 𝑦 ∈ On ∧ ω ∈ On) →
((ω ↑𝑜 𝑥) ·𝑜 (𝑦 +𝑜 ω))
= (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜
((ω ↑𝑜 𝑥) ·𝑜
ω))) |
76 | 59, 61, 74, 75 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → ((ω
↑𝑜 𝑥) ·𝑜 (𝑦 +𝑜 ω))
= (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜
((ω ↑𝑜 𝑥) ·𝑜
ω))) |
77 | | simprl 790 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → 𝑦 ∈ ω) |
78 | | oaabslem 7610 |
. . . . . . . . . . . . . . . . 17
⊢ ((ω
∈ On ∧ 𝑦 ∈
ω) → (𝑦
+𝑜 ω) = ω) |
79 | 74, 77, 78 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → (𝑦 +𝑜 ω) =
ω) |
80 | 79 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → ((ω
↑𝑜 𝑥) ·𝑜 (𝑦 +𝑜 ω))
= ((ω ↑𝑜 𝑥) ·𝑜
ω)) |
81 | 76, 80 | eqtr3d 2646 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → (((ω
↑𝑜 𝑥) ·𝑜 𝑦) +𝑜
((ω ↑𝑜 𝑥) ·𝑜 ω)) =
((ω ↑𝑜 𝑥) ·𝑜
ω)) |
82 | 55 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → (ω
↑𝑜 𝐶) = ((ω ↑𝑜
𝑥)
·𝑜 ω)) |
83 | 82 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → (((ω
↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω
↑𝑜 𝐶)) = (((ω ↑𝑜
𝑥)
·𝑜 𝑦) +𝑜 ((ω
↑𝑜 𝑥) ·𝑜
ω))) |
84 | 81, 83, 82 | 3eqtr4d 2654 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → (((ω
↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω
↑𝑜 𝐶)) = (ω ↑𝑜
𝐶)) |
85 | 73, 84 | sseqtrd 3604 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜
𝑥)
·𝑜 𝑦))) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) ⊆ (ω
↑𝑜 𝐶)) |
86 | 58, 85 | rexlimddv 3017 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) ⊆ (ω
↑𝑜 𝐶)) |
87 | | oaword2 7520 |
. . . . . . . . . . . . 13
⊢
(((ω ↑𝑜 𝐶) ∈ On ∧ 𝐴 ∈ On) → (ω
↑𝑜 𝐶) ⊆ (𝐴 +𝑜 (ω
↑𝑜 𝐶))) |
88 | 9, 18, 87 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜
𝐶) ⊆ (𝐴 +𝑜 (ω
↑𝑜 𝐶))) |
89 | 88 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜
𝐶) ⊆ (𝐴 +𝑜 (ω
↑𝑜 𝐶))) |
90 | 86, 89 | eqssd 3585 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) = (ω ↑𝑜
𝐶)) |
91 | 90 | rexlimdvaa 3014 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → (∃𝑥 ∈ On 𝐶 = suc 𝑥 → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) = (ω ↑𝑜
𝐶))) |
92 | | simplll 794 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐴 ∈ (ω ↑𝑜
𝐶)) |
93 | 31 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → ω ∈ On) |
94 | 24 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐶 ∈ On) |
95 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → Lim 𝐶) |
96 | | oelim2 7562 |
. . . . . . . . . . . . . . 15
⊢ ((ω
∈ On ∧ (𝐶 ∈
On ∧ Lim 𝐶)) →
(ω ↑𝑜 𝐶) = ∪
𝑥 ∈ (𝐶 ∖ 1𝑜)(ω
↑𝑜 𝑥)) |
97 | 93, 94, 95, 96 | syl12anc 1316 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑𝑜
𝐶) = ∪ 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω
↑𝑜 𝑥)) |
98 | 92, 97 | eleqtrd 2690 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐴 ∈ ∪
𝑥 ∈ (𝐶 ∖ 1𝑜)(ω
↑𝑜 𝑥)) |
99 | | eliun 4460 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ∪ 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω
↑𝑜 𝑥) ↔ ∃𝑥 ∈ (𝐶 ∖ 1𝑜)𝐴 ∈ (ω
↑𝑜 𝑥)) |
100 | 98, 99 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → ∃𝑥 ∈ (𝐶 ∖ 1𝑜)𝐴 ∈ (ω
↑𝑜 𝑥)) |
101 | | eldifi 3694 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐶 ∖ 1𝑜) → 𝑥 ∈ 𝐶) |
102 | 18 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) → 𝐴 ∈ On) |
103 | 9 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) → (ω
↑𝑜 𝐶) ∈ On) |
104 | 93 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) → ω ∈
On) |
105 | | 1onn 7606 |
. . . . . . . . . . . . . . . . . . . 20
⊢
1𝑜 ∈ ω |
106 | 105 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) →
1𝑜 ∈ ω) |
107 | | ondif2 7469 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ω
∈ (On ∖ 2𝑜) ↔ (ω ∈ On ∧
1𝑜 ∈ ω)) |
108 | 104, 106,
107 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) → ω ∈
(On ∖ 2𝑜)) |
109 | 94 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) → 𝐶 ∈ On) |
110 | | simplr 788 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) → Lim 𝐶) |
111 | | oelimcl 7567 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ω
∈ (On ∖ 2𝑜) ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → Lim (ω
↑𝑜 𝐶)) |
112 | 108, 109,
110, 111 | syl12anc 1316 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) → Lim (ω
↑𝑜 𝐶)) |
113 | | oalim 7499 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ On ∧ ((ω
↑𝑜 𝐶) ∈ On ∧ Lim (ω
↑𝑜 𝐶))) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) = ∪
𝑦 ∈ (ω
↑𝑜 𝐶)(𝐴 +𝑜 𝑦)) |
114 | 102, 103,
112, 113 | syl12anc 1316 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) = ∪
𝑦 ∈ (ω
↑𝑜 𝐶)(𝐴 +𝑜 𝑦)) |
115 | | oelim2 7562 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ω
∈ On ∧ (𝐶 ∈
On ∧ Lim 𝐶)) →
(ω ↑𝑜 𝐶) = ∪
𝑧 ∈ (𝐶 ∖ 1𝑜)(ω
↑𝑜 𝑧)) |
116 | 93, 94, 95, 115 | syl12anc 1316 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑𝑜
𝐶) = ∪ 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω
↑𝑜 𝑧)) |
117 | 116 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝑦 ∈ (ω ↑𝑜
𝐶) ↔ 𝑦 ∈ ∪ 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω
↑𝑜 𝑧))) |
118 | | eliun 4460 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ∪ 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω
↑𝑜 𝑧) ↔ ∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω
↑𝑜 𝑧)) |
119 | 117, 118 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝑦 ∈ (ω ↑𝑜
𝐶) ↔ ∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω
↑𝑜 𝑧))) |
120 | 119 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) → (𝑦 ∈ (ω
↑𝑜 𝐶) ↔ ∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω
↑𝑜 𝑧))) |
121 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ (𝐶 ∖ 1𝑜) → 𝑧 ∈ 𝐶) |
122 | 104 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → ω ∈
On) |
123 | 109 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → 𝐶 ∈ On) |
124 | | simplrl 796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → 𝑥 ∈ 𝐶) |
125 | | onelon 5665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ On) |
126 | 123, 124,
125 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → 𝑥 ∈ On) |
127 | 122, 126,
46 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (ω
↑𝑜 𝑥) ∈ On) |
128 | | eloni 5650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((ω
↑𝑜 𝑥) ∈ On → Ord (ω
↑𝑜 𝑥)) |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → Ord (ω
↑𝑜 𝑥)) |
130 | | simplrr 797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → 𝐴 ∈ (ω
↑𝑜 𝑥)) |
131 | | ordelss 5656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((Ord
(ω ↑𝑜 𝑥) ∧ 𝐴 ∈ (ω ↑𝑜
𝑥)) → 𝐴 ⊆ (ω
↑𝑜 𝑥)) |
132 | 129, 130,
131 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → 𝐴 ⊆ (ω
↑𝑜 𝑥)) |
133 | | ssun1 3738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑥 ⊆ (𝑥 ∪ 𝑧) |
134 | 26 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → Ord 𝐶) |
135 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → 𝑧 ∈ 𝐶) |
136 | | ordunel 6919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((Ord
𝐶 ∧ 𝑥 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶) → (𝑥 ∪ 𝑧) ∈ 𝐶) |
137 | 134, 124,
135, 136 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (𝑥 ∪ 𝑧) ∈ 𝐶) |
138 | | onelon 5665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐶 ∈ On ∧ (𝑥 ∪ 𝑧) ∈ 𝐶) → (𝑥 ∪ 𝑧) ∈ On) |
139 | 123, 137,
138 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (𝑥 ∪ 𝑧) ∈ On) |
140 | | peano1 6977 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ∅
∈ ω |
141 | 140 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → ∅ ∈
ω) |
142 | | oewordi 7558 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 ∈ On ∧ (𝑥 ∪ 𝑧) ∈ On ∧ ω ∈ On) ∧
∅ ∈ ω) → (𝑥 ⊆ (𝑥 ∪ 𝑧) → (ω ↑𝑜
𝑥) ⊆ (ω
↑𝑜 (𝑥 ∪ 𝑧)))) |
143 | 126, 139,
122, 141, 142 | syl31anc 1321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (𝑥 ⊆ (𝑥 ∪ 𝑧) → (ω ↑𝑜
𝑥) ⊆ (ω
↑𝑜 (𝑥 ∪ 𝑧)))) |
144 | 133, 143 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (ω
↑𝑜 𝑥) ⊆ (ω ↑𝑜
(𝑥 ∪ 𝑧))) |
145 | 132, 144 | sstrd 3578 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → 𝐴 ⊆ (ω
↑𝑜 (𝑥 ∪ 𝑧))) |
146 | 102 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → 𝐴 ∈ On) |
147 | | oecl 7504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((ω
∈ On ∧ (𝑥 ∪
𝑧) ∈ On) →
(ω ↑𝑜 (𝑥 ∪ 𝑧)) ∈ On) |
148 | 122, 139,
147 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (ω
↑𝑜 (𝑥 ∪ 𝑧)) ∈ On) |
149 | | onelon 5665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐶 ∈ On ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ On) |
150 | 123, 135,
149 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → 𝑧 ∈ On) |
151 | | oecl 7504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((ω
∈ On ∧ 𝑧 ∈
On) → (ω ↑𝑜 𝑧) ∈ On) |
152 | 122, 150,
151 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (ω
↑𝑜 𝑧) ∈ On) |
153 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → 𝑦 ∈ (ω
↑𝑜 𝑧)) |
154 | | onelon 5665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((ω ↑𝑜 𝑧) ∈ On ∧ 𝑦 ∈ (ω ↑𝑜
𝑧)) → 𝑦 ∈ On) |
155 | 152, 153,
154 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → 𝑦 ∈ On) |
156 | | oawordri 7517 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ On ∧ (ω
↑𝑜 (𝑥 ∪ 𝑧)) ∈ On ∧ 𝑦 ∈ On) → (𝐴 ⊆ (ω ↑𝑜
(𝑥 ∪ 𝑧)) → (𝐴 +𝑜 𝑦) ⊆ ((ω
↑𝑜 (𝑥 ∪ 𝑧)) +𝑜 𝑦))) |
157 | 146, 148,
155, 156 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (𝐴 ⊆ (ω
↑𝑜 (𝑥 ∪ 𝑧)) → (𝐴 +𝑜 𝑦) ⊆ ((ω
↑𝑜 (𝑥 ∪ 𝑧)) +𝑜 𝑦))) |
158 | 145, 157 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (𝐴 +𝑜 𝑦) ⊆ ((ω
↑𝑜 (𝑥 ∪ 𝑧)) +𝑜 𝑦)) |
159 | | eloni 5650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((ω
↑𝑜 𝑧) ∈ On → Ord (ω
↑𝑜 𝑧)) |
160 | 152, 159 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → Ord (ω
↑𝑜 𝑧)) |
161 | | ordelss 5656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((Ord
(ω ↑𝑜 𝑧) ∧ 𝑦 ∈ (ω ↑𝑜
𝑧)) → 𝑦 ⊆ (ω
↑𝑜 𝑧)) |
162 | 160, 153,
161 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → 𝑦 ⊆ (ω
↑𝑜 𝑧)) |
163 | | ssun2 3739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑧 ⊆ (𝑥 ∪ 𝑧) |
164 | | oewordi 7558 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑧 ∈ On ∧ (𝑥 ∪ 𝑧) ∈ On ∧ ω ∈ On) ∧
∅ ∈ ω) → (𝑧 ⊆ (𝑥 ∪ 𝑧) → (ω ↑𝑜
𝑧) ⊆ (ω
↑𝑜 (𝑥 ∪ 𝑧)))) |
165 | 150, 139,
122, 141, 164 | syl31anc 1321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (𝑧 ⊆ (𝑥 ∪ 𝑧) → (ω ↑𝑜
𝑧) ⊆ (ω
↑𝑜 (𝑥 ∪ 𝑧)))) |
166 | 163, 165 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (ω
↑𝑜 𝑧) ⊆ (ω ↑𝑜
(𝑥 ∪ 𝑧))) |
167 | 162, 166 | sstrd 3578 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → 𝑦 ⊆ (ω
↑𝑜 (𝑥 ∪ 𝑧))) |
168 | | oaword 7516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ On ∧ (ω
↑𝑜 (𝑥 ∪ 𝑧)) ∈ On ∧ (ω
↑𝑜 (𝑥 ∪ 𝑧)) ∈ On) → (𝑦 ⊆ (ω ↑𝑜
(𝑥 ∪ 𝑧)) ↔ ((ω
↑𝑜 (𝑥 ∪ 𝑧)) +𝑜 𝑦) ⊆ ((ω
↑𝑜 (𝑥 ∪ 𝑧)) +𝑜 (ω
↑𝑜 (𝑥 ∪ 𝑧))))) |
169 | 155, 148,
148, 168 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (𝑦 ⊆ (ω
↑𝑜 (𝑥 ∪ 𝑧)) ↔ ((ω
↑𝑜 (𝑥 ∪ 𝑧)) +𝑜 𝑦) ⊆ ((ω
↑𝑜 (𝑥 ∪ 𝑧)) +𝑜 (ω
↑𝑜 (𝑥 ∪ 𝑧))))) |
170 | 167, 169 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → ((ω
↑𝑜 (𝑥 ∪ 𝑧)) +𝑜 𝑦) ⊆ ((ω
↑𝑜 (𝑥 ∪ 𝑧)) +𝑜 (ω
↑𝑜 (𝑥 ∪ 𝑧)))) |
171 | 158, 170 | sstrd 3578 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (𝐴 +𝑜 𝑦) ⊆ ((ω
↑𝑜 (𝑥 ∪ 𝑧)) +𝑜 (ω
↑𝑜 (𝑥 ∪ 𝑧)))) |
172 | | ordom 6966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ Ord
ω |
173 | | ordsucss 6910 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (Ord
ω → (1𝑜 ∈ ω → suc
1𝑜 ⊆ ω)) |
174 | 172, 105,
173 | mp2 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ suc
1𝑜 ⊆ ω |
175 | | 1on 7454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
1𝑜 ∈ On |
176 | | suceloni 6905 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(1𝑜 ∈ On → suc 1𝑜 ∈
On) |
177 | 175, 176 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → suc
1𝑜 ∈ On) |
178 | | omwordi 7538 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((suc
1𝑜 ∈ On ∧ ω ∈ On ∧ (ω
↑𝑜 (𝑥 ∪ 𝑧)) ∈ On) → (suc
1𝑜 ⊆ ω → ((ω
↑𝑜 (𝑥 ∪ 𝑧)) ·𝑜 suc
1𝑜) ⊆ ((ω ↑𝑜 (𝑥 ∪ 𝑧)) ·𝑜
ω))) |
179 | 177, 122,
148, 178 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (suc
1𝑜 ⊆ ω → ((ω
↑𝑜 (𝑥 ∪ 𝑧)) ·𝑜 suc
1𝑜) ⊆ ((ω ↑𝑜 (𝑥 ∪ 𝑧)) ·𝑜
ω))) |
180 | 174, 179 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → ((ω
↑𝑜 (𝑥 ∪ 𝑧)) ·𝑜 suc
1𝑜) ⊆ ((ω ↑𝑜 (𝑥 ∪ 𝑧)) ·𝑜
ω)) |
181 | 175 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) →
1𝑜 ∈ On) |
182 | | omsuc 7493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((ω ↑𝑜 (𝑥 ∪ 𝑧)) ∈ On ∧ 1𝑜
∈ On) → ((ω ↑𝑜 (𝑥 ∪ 𝑧)) ·𝑜 suc
1𝑜) = (((ω ↑𝑜 (𝑥 ∪ 𝑧)) ·𝑜
1𝑜) +𝑜 (ω
↑𝑜 (𝑥 ∪ 𝑧)))) |
183 | 148, 181,
182 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → ((ω
↑𝑜 (𝑥 ∪ 𝑧)) ·𝑜 suc
1𝑜) = (((ω ↑𝑜 (𝑥 ∪ 𝑧)) ·𝑜
1𝑜) +𝑜 (ω
↑𝑜 (𝑥 ∪ 𝑧)))) |
184 | | om1 7509 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((ω
↑𝑜 (𝑥 ∪ 𝑧)) ∈ On → ((ω
↑𝑜 (𝑥 ∪ 𝑧)) ·𝑜
1𝑜) = (ω ↑𝑜 (𝑥 ∪ 𝑧))) |
185 | 148, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → ((ω
↑𝑜 (𝑥 ∪ 𝑧)) ·𝑜
1𝑜) = (ω ↑𝑜 (𝑥 ∪ 𝑧))) |
186 | 185 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (((ω
↑𝑜 (𝑥 ∪ 𝑧)) ·𝑜
1𝑜) +𝑜 (ω
↑𝑜 (𝑥 ∪ 𝑧))) = ((ω ↑𝑜
(𝑥 ∪ 𝑧)) +𝑜 (ω
↑𝑜 (𝑥 ∪ 𝑧)))) |
187 | 183, 186 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → ((ω
↑𝑜 (𝑥 ∪ 𝑧)) +𝑜 (ω
↑𝑜 (𝑥 ∪ 𝑧))) = ((ω ↑𝑜
(𝑥 ∪ 𝑧)) ·𝑜 suc
1𝑜)) |
188 | | oesuc 7494 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((ω
∈ On ∧ (𝑥 ∪
𝑧) ∈ On) →
(ω ↑𝑜 suc (𝑥 ∪ 𝑧)) = ((ω ↑𝑜
(𝑥 ∪ 𝑧)) ·𝑜
ω)) |
189 | 122, 139,
188 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (ω
↑𝑜 suc (𝑥 ∪ 𝑧)) = ((ω ↑𝑜
(𝑥 ∪ 𝑧)) ·𝑜
ω)) |
190 | 180, 187,
189 | 3sstr4d 3611 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → ((ω
↑𝑜 (𝑥 ∪ 𝑧)) +𝑜 (ω
↑𝑜 (𝑥 ∪ 𝑧))) ⊆ (ω
↑𝑜 suc (𝑥 ∪ 𝑧))) |
191 | 171, 190 | sstrd 3578 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (𝐴 +𝑜 𝑦) ⊆ (ω
↑𝑜 suc (𝑥 ∪ 𝑧))) |
192 | | ordsucss 6910 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Ord
𝐶 → ((𝑥 ∪ 𝑧) ∈ 𝐶 → suc (𝑥 ∪ 𝑧) ⊆ 𝐶)) |
193 | 134, 137,
192 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → suc (𝑥 ∪ 𝑧) ⊆ 𝐶) |
194 | | suceloni 6905 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∪ 𝑧) ∈ On → suc (𝑥 ∪ 𝑧) ∈ On) |
195 | 139, 194 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → suc (𝑥 ∪ 𝑧) ∈ On) |
196 | | oewordi 7558 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((suc
(𝑥 ∪ 𝑧) ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ On) ∧
∅ ∈ ω) → (suc (𝑥 ∪ 𝑧) ⊆ 𝐶 → (ω ↑𝑜
suc (𝑥 ∪ 𝑧)) ⊆ (ω
↑𝑜 𝐶))) |
197 | 195, 123,
122, 141, 196 | syl31anc 1321 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (suc (𝑥 ∪ 𝑧) ⊆ 𝐶 → (ω ↑𝑜
suc (𝑥 ∪ 𝑧)) ⊆ (ω
↑𝑜 𝐶))) |
198 | 193, 197 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (ω
↑𝑜 suc (𝑥 ∪ 𝑧)) ⊆ (ω
↑𝑜 𝐶)) |
199 | 191, 198 | sstrd 3578 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑𝑜
𝑧))) → (𝐴 +𝑜 𝑦) ⊆ (ω
↑𝑜 𝐶)) |
200 | 199 | expr 641 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ 𝑧 ∈ 𝐶) → (𝑦 ∈ (ω ↑𝑜
𝑧) → (𝐴 +𝑜 𝑦) ⊆ (ω
↑𝑜 𝐶))) |
201 | 121, 200 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) ∧ 𝑧 ∈ (𝐶 ∖ 1𝑜)) →
(𝑦 ∈ (ω
↑𝑜 𝑧) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜
𝐶))) |
202 | 201 | rexlimdva 3013 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) → (∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω
↑𝑜 𝑧) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜
𝐶))) |
203 | 120, 202 | sylbid 229 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) → (𝑦 ∈ (ω
↑𝑜 𝐶) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜
𝐶))) |
204 | 203 | ralrimiv 2948 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) → ∀𝑦 ∈ (ω
↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜
𝐶)) |
205 | | iunss 4497 |
. . . . . . . . . . . . . . . . 17
⊢ (∪ 𝑦 ∈ (ω ↑𝑜
𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜
𝐶) ↔ ∀𝑦 ∈ (ω
↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜
𝐶)) |
206 | 204, 205 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) → ∪ 𝑦 ∈ (ω ↑𝑜
𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜
𝐶)) |
207 | 114, 206 | eqsstrd 3602 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑𝑜
𝑥))) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) ⊆ (ω
↑𝑜 𝐶)) |
208 | 207 | expr 641 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ 𝑥 ∈ 𝐶) → (𝐴 ∈ (ω ↑𝑜
𝑥) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) ⊆ (ω
↑𝑜 𝐶))) |
209 | 101, 208 | sylan2 490 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
(ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ 𝑥 ∈ (𝐶 ∖ 1𝑜)) →
(𝐴 ∈ (ω
↑𝑜 𝑥) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) ⊆ (ω
↑𝑜 𝐶))) |
210 | 209 | rexlimdva 3013 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (∃𝑥 ∈ (𝐶 ∖ 1𝑜)𝐴 ∈ (ω
↑𝑜 𝑥) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) ⊆ (ω
↑𝑜 𝐶))) |
211 | 100, 210 | mpd 15 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) ⊆ (ω
↑𝑜 𝐶)) |
212 | 88 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑𝑜
𝐶) ⊆ (𝐴 +𝑜 (ω
↑𝑜 𝐶))) |
213 | 211, 212 | eqssd 3585 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) = (ω ↑𝑜
𝐶)) |
214 | 213 | ex 449 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → (Lim 𝐶 → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) = (ω ↑𝑜
𝐶))) |
215 | 43, 91, 214 | 3jaod 1384 |
. . . . . . . 8
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → ((𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) = (ω ↑𝑜
𝐶))) |
216 | 28, 215 | mpd 15 |
. . . . . . 7
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) = (ω ↑𝑜
𝐶)) |
217 | 216 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +𝑜 (ω
↑𝑜 𝐶)) = (ω ↑𝑜
𝐶)) |
218 | 217 | oveq1d 6564 |
. . . . 5
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +𝑜 (ω
↑𝑜 𝐶)) +𝑜 𝑥) = ((ω ↑𝑜
𝐶) +𝑜
𝑥)) |
219 | 23, 218 | eqtr3d 2646 |
. . . 4
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +𝑜 ((ω
↑𝑜 𝐶) +𝑜 𝑥)) = ((ω ↑𝑜
𝐶) +𝑜
𝑥)) |
220 | | oveq2 6557 |
. . . . 5
⊢
(((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → (𝐴 +𝑜 ((ω
↑𝑜 𝐶) +𝑜 𝑥)) = (𝐴 +𝑜 𝐵)) |
221 | | id 22 |
. . . . 5
⊢
(((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → ((ω ↑𝑜
𝐶) +𝑜
𝑥) = 𝐵) |
222 | 220, 221 | eqeq12d 2625 |
. . . 4
⊢
(((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → ((𝐴 +𝑜 ((ω
↑𝑜 𝐶) +𝑜 𝑥)) = ((ω ↑𝑜
𝐶) +𝑜
𝑥) ↔ (𝐴 +𝑜 𝐵) = 𝐵)) |
223 | 219, 222 | syl5ibcom 234 |
. . 3
⊢ ((((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (((ω
↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → (𝐴 +𝑜 𝐵) = 𝐵)) |
224 | 223 | rexlimdva 3013 |
. 2
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → (∃𝑥 ∈ On ((ω
↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → (𝐴 +𝑜 𝐵) = 𝐵)) |
225 | 15, 224 | mpd 15 |
1
⊢ (((𝐴 ∈ (ω
↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑𝑜 𝐶) ⊆ 𝐵) → (𝐴 +𝑜 𝐵) = 𝐵) |