Step | Hyp | Ref
| Expression |
1 | | n0i 4248 |
. . . . . . 7
⊢ (𝐴 ∈ (ω
↑o 𝐶)
→ ¬ (ω ↑o 𝐶) = ∅) |
2 | | fnoe 8237 |
. . . . . . . . 9
⊢
↑o Fn (On × On) |
3 | | fndm 6481 |
. . . . . . . . 9
⊢ (
↑o Fn (On × On) → dom ↑o = (On
× On)) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . 8
⊢ dom
↑o = (On × On) |
5 | 4 | ndmov 7392 |
. . . . . . 7
⊢ (¬
(ω ∈ On ∧ 𝐶
∈ On) → (ω ↑o 𝐶) = ∅) |
6 | 1, 5 | nsyl2 143 |
. . . . . 6
⊢ (𝐴 ∈ (ω
↑o 𝐶)
→ (ω ∈ On ∧ 𝐶 ∈ On)) |
7 | 6 | ad2antrr 726 |
. . . . 5
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) → (ω
∈ On ∧ 𝐶 ∈
On)) |
8 | | oecl 8264 |
. . . . 5
⊢ ((ω
∈ On ∧ 𝐶 ∈
On) → (ω ↑o 𝐶) ∈ On) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) → (ω
↑o 𝐶)
∈ On) |
10 | | simplr 769 |
. . . 4
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) → 𝐵 ∈ On) |
11 | | simpr 488 |
. . . 4
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) → (ω
↑o 𝐶)
⊆ 𝐵) |
12 | | oawordeu 8283 |
. . . 4
⊢
((((ω ↑o 𝐶) ∈ On ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) →
∃!𝑥 ∈ On
((ω ↑o 𝐶) +o 𝑥) = 𝐵) |
13 | 9, 10, 11, 12 | syl21anc 838 |
. . 3
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) →
∃!𝑥 ∈ On
((ω ↑o 𝐶) +o 𝑥) = 𝐵) |
14 | | reurex 3338 |
. . 3
⊢
(∃!𝑥 ∈ On
((ω ↑o 𝐶) +o 𝑥) = 𝐵 → ∃𝑥 ∈ On ((ω ↑o 𝐶) +o 𝑥) = 𝐵) |
15 | 13, 14 | syl 17 |
. 2
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) →
∃𝑥 ∈ On
((ω ↑o 𝐶) +o 𝑥) = 𝐵) |
16 | | simpll 767 |
. . . . . . . 8
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) → 𝐴 ∈ (ω
↑o 𝐶)) |
17 | | onelon 6238 |
. . . . . . . 8
⊢
(((ω ↑o 𝐶) ∈ On ∧ 𝐴 ∈ (ω ↑o 𝐶)) → 𝐴 ∈ On) |
18 | 9, 16, 17 | syl2anc 587 |
. . . . . . 7
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) → 𝐴 ∈ On) |
19 | 18 | adantr 484 |
. . . . . 6
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝐴 ∈ On) |
20 | 9 | adantr 484 |
. . . . . 6
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ 𝑥 ∈ On) → (ω
↑o 𝐶)
∈ On) |
21 | | simpr 488 |
. . . . . 6
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝑥 ∈ On) |
22 | | oaass 8289 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ (ω
↑o 𝐶)
∈ On ∧ 𝑥 ∈
On) → ((𝐴
+o (ω ↑o 𝐶)) +o 𝑥) = (𝐴 +o ((ω ↑o
𝐶) +o 𝑥))) |
23 | 19, 20, 21, 22 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +o (ω
↑o 𝐶))
+o 𝑥) = (𝐴 +o ((ω
↑o 𝐶)
+o 𝑥))) |
24 | 7 | simprd 499 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) → 𝐶 ∈ On) |
25 | | eloni 6223 |
. . . . . . . . . 10
⊢ (𝐶 ∈ On → Ord 𝐶) |
26 | 24, 25 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) → Ord 𝐶) |
27 | | ordzsl 7624 |
. . . . . . . . 9
⊢ (Ord
𝐶 ↔ (𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶)) |
28 | 26, 27 | sylib 221 |
. . . . . . . 8
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) → (𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶)) |
29 | | simplll 775 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 ∈ (ω
↑o 𝐶)) |
30 | | oveq2 7221 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 = ∅ → (ω
↑o 𝐶) =
(ω ↑o ∅)) |
31 | 7 | simpld 498 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) → ω
∈ On) |
32 | | oe0 8249 |
. . . . . . . . . . . . . . . 16
⊢ (ω
∈ On → (ω ↑o ∅) =
1o) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) → (ω
↑o ∅) = 1o) |
34 | 30, 33 | sylan9eqr 2800 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ 𝐶 = ∅) → (ω
↑o 𝐶) =
1o) |
35 | 29, 34 | eleqtrd 2840 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 ∈
1o) |
36 | | el1o 8226 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 1o ↔
𝐴 =
∅) |
37 | 35, 36 | sylib 221 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 = ∅) |
38 | 37 | oveq1d 7228 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ 𝐶 = ∅) → (𝐴 +o (ω
↑o 𝐶)) =
(∅ +o (ω ↑o 𝐶))) |
39 | 9 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ 𝐶 = ∅) → (ω
↑o 𝐶)
∈ On) |
40 | | oa0r 8265 |
. . . . . . . . . . . 12
⊢ ((ω
↑o 𝐶)
∈ On → (∅ +o (ω ↑o 𝐶)) = (ω ↑o
𝐶)) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ 𝐶 = ∅) → (∅
+o (ω ↑o 𝐶)) = (ω ↑o 𝐶)) |
42 | 38, 41 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ 𝐶 = ∅) → (𝐴 +o (ω
↑o 𝐶)) =
(ω ↑o 𝐶)) |
43 | 42 | ex 416 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) → (𝐶 = ∅ → (𝐴 +o (ω
↑o 𝐶)) =
(ω ↑o 𝐶))) |
44 | 31 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → ω ∈ On) |
45 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝑥 ∈ On) |
46 | | oecl 8264 |
. . . . . . . . . . . . . 14
⊢ ((ω
∈ On ∧ 𝑥 ∈
On) → (ω ↑o 𝑥) ∈ On) |
47 | 44, 45, 46 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑o 𝑥) ∈ On) |
48 | | limom 7660 |
. . . . . . . . . . . . . 14
⊢ Lim
ω |
49 | 44, 48 | jctir 524 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ∈ On ∧ Lim
ω)) |
50 | | simplll 775 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐴 ∈ (ω ↑o 𝐶)) |
51 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐶 = suc 𝑥) |
52 | 51 | oveq2d 7229 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑o 𝐶) = (ω ↑o
suc 𝑥)) |
53 | | oesuc 8254 |
. . . . . . . . . . . . . . . 16
⊢ ((ω
∈ On ∧ 𝑥 ∈
On) → (ω ↑o suc 𝑥) = ((ω ↑o 𝑥) ·o
ω)) |
54 | 44, 45, 53 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑o suc
𝑥) = ((ω
↑o 𝑥)
·o ω)) |
55 | 52, 54 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑o 𝐶) = ((ω ↑o
𝑥) ·o
ω)) |
56 | 50, 55 | eleqtrd 2840 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐴 ∈ ((ω ↑o 𝑥) ·o
ω)) |
57 | | omordlim 8305 |
. . . . . . . . . . . . 13
⊢
((((ω ↑o 𝑥) ∈ On ∧ (ω ∈ On ∧
Lim ω)) ∧ 𝐴
∈ ((ω ↑o 𝑥) ·o ω)) →
∃𝑦 ∈ ω
𝐴 ∈ ((ω
↑o 𝑥)
·o 𝑦)) |
58 | 47, 49, 56, 57 | syl21anc 838 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → ∃𝑦 ∈ ω 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦)) |
59 | 47 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (ω
↑o 𝑥)
∈ On) |
60 | | nnon 7650 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ω → 𝑦 ∈ On) |
61 | 60 | ad2antrl 728 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → 𝑦 ∈ On) |
62 | | omcl 8263 |
. . . . . . . . . . . . . . . . 17
⊢
(((ω ↑o 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω
↑o 𝑥)
·o 𝑦)
∈ On) |
63 | 59, 61, 62 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → ((ω
↑o 𝑥)
·o 𝑦)
∈ On) |
64 | | eloni 6223 |
. . . . . . . . . . . . . . . 16
⊢
(((ω ↑o 𝑥) ·o 𝑦) ∈ On → Ord ((ω
↑o 𝑥)
·o 𝑦)) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → Ord ((ω
↑o 𝑥)
·o 𝑦)) |
66 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦)) |
67 | | ordelss 6229 |
. . . . . . . . . . . . . . 15
⊢ ((Ord
((ω ↑o 𝑥) ·o 𝑦) ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦)) → 𝐴 ⊆ ((ω ↑o 𝑥) ·o 𝑦)) |
68 | 65, 66, 67 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → 𝐴 ⊆ ((ω ↑o 𝑥) ·o 𝑦)) |
69 | 18 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → 𝐴 ∈ On) |
70 | 9 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (ω
↑o 𝐶)
∈ On) |
71 | | oawordri 8278 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ On ∧ ((ω
↑o 𝑥)
·o 𝑦)
∈ On ∧ (ω ↑o 𝐶) ∈ On) → (𝐴 ⊆ ((ω ↑o 𝑥) ·o 𝑦) → (𝐴 +o (ω ↑o
𝐶)) ⊆ (((ω
↑o 𝑥)
·o 𝑦)
+o (ω ↑o 𝐶)))) |
72 | 69, 63, 70, 71 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (𝐴 ⊆ ((ω ↑o 𝑥) ·o 𝑦) → (𝐴 +o (ω ↑o
𝐶)) ⊆ (((ω
↑o 𝑥)
·o 𝑦)
+o (ω ↑o 𝐶)))) |
73 | 68, 72 | mpd 15 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (𝐴 +o (ω ↑o
𝐶)) ⊆ (((ω
↑o 𝑥)
·o 𝑦)
+o (ω ↑o 𝐶))) |
74 | 44 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → ω ∈
On) |
75 | | odi 8307 |
. . . . . . . . . . . . . . . 16
⊢
(((ω ↑o 𝑥) ∈ On ∧ 𝑦 ∈ On ∧ ω ∈ On) →
((ω ↑o 𝑥) ·o (𝑦 +o ω)) = (((ω
↑o 𝑥)
·o 𝑦)
+o ((ω ↑o 𝑥) ·o
ω))) |
76 | 59, 61, 74, 75 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → ((ω
↑o 𝑥)
·o (𝑦
+o ω)) = (((ω ↑o 𝑥) ·o 𝑦) +o ((ω ↑o
𝑥) ·o
ω))) |
77 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → 𝑦 ∈ ω) |
78 | | oaabslem 8372 |
. . . . . . . . . . . . . . . . 17
⊢ ((ω
∈ On ∧ 𝑦 ∈
ω) → (𝑦
+o ω) = ω) |
79 | 74, 77, 78 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (𝑦 +o ω) =
ω) |
80 | 79 | oveq2d 7229 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → ((ω
↑o 𝑥)
·o (𝑦
+o ω)) = ((ω ↑o 𝑥) ·o
ω)) |
81 | 76, 80 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (((ω
↑o 𝑥)
·o 𝑦)
+o ((ω ↑o 𝑥) ·o ω)) = ((ω
↑o 𝑥)
·o ω)) |
82 | 55 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (ω
↑o 𝐶) =
((ω ↑o 𝑥) ·o
ω)) |
83 | 82 | oveq2d 7229 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (((ω
↑o 𝑥)
·o 𝑦)
+o (ω ↑o 𝐶)) = (((ω ↑o 𝑥) ·o 𝑦) +o ((ω
↑o 𝑥)
·o ω))) |
84 | 81, 83, 82 | 3eqtr4d 2787 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (((ω
↑o 𝑥)
·o 𝑦)
+o (ω ↑o 𝐶)) = (ω ↑o 𝐶)) |
85 | 73, 84 | sseqtrd 3941 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (𝐴 +o (ω ↑o
𝐶)) ⊆ (ω
↑o 𝐶)) |
86 | 58, 85 | rexlimddv 3210 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (𝐴 +o (ω ↑o
𝐶)) ⊆ (ω
↑o 𝐶)) |
87 | | oaword2 8281 |
. . . . . . . . . . . . 13
⊢
(((ω ↑o 𝐶) ∈ On ∧ 𝐴 ∈ On) → (ω
↑o 𝐶)
⊆ (𝐴 +o
(ω ↑o 𝐶))) |
88 | 9, 18, 87 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) → (ω
↑o 𝐶)
⊆ (𝐴 +o
(ω ↑o 𝐶))) |
89 | 88 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑o 𝐶) ⊆ (𝐴 +o (ω ↑o
𝐶))) |
90 | 86, 89 | eqssd 3918 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (𝐴 +o (ω ↑o
𝐶)) = (ω
↑o 𝐶)) |
91 | 90 | rexlimdvaa 3204 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) →
(∃𝑥 ∈ On 𝐶 = suc 𝑥 → (𝐴 +o (ω ↑o
𝐶)) = (ω
↑o 𝐶))) |
92 | | simplll 775 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) → 𝐴 ∈ (ω ↑o 𝐶)) |
93 | 31 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) → ω ∈
On) |
94 | 24 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) → 𝐶 ∈ On) |
95 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) → Lim 𝐶) |
96 | | oelim2 8323 |
. . . . . . . . . . . . . . 15
⊢ ((ω
∈ On ∧ (𝐶 ∈
On ∧ Lim 𝐶)) →
(ω ↑o 𝐶) = ∪
𝑥 ∈ (𝐶 ∖ 1o)(ω
↑o 𝑥)) |
97 | 93, 94, 95, 96 | syl12anc 837 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) → (ω
↑o 𝐶) =
∪ 𝑥 ∈ (𝐶 ∖ 1o)(ω
↑o 𝑥)) |
98 | 92, 97 | eleqtrd 2840 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) → 𝐴 ∈ ∪
𝑥 ∈ (𝐶 ∖ 1o)(ω
↑o 𝑥)) |
99 | | eliun 4908 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ∪ 𝑥 ∈ (𝐶 ∖ 1o)(ω
↑o 𝑥)
↔ ∃𝑥 ∈
(𝐶 ∖
1o)𝐴 ∈
(ω ↑o 𝑥)) |
100 | 98, 99 | sylib 221 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) → ∃𝑥 ∈ (𝐶 ∖ 1o)𝐴 ∈ (ω ↑o 𝑥)) |
101 | | eldifi 4041 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐶 ∖ 1o) → 𝑥 ∈ 𝐶) |
102 | 18 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) → 𝐴 ∈ On) |
103 | 9 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) → (ω
↑o 𝐶)
∈ On) |
104 | 93 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) → ω ∈
On) |
105 | | 1onn 8367 |
. . . . . . . . . . . . . . . . . . 19
⊢
1o ∈ ω |
106 | | ondif2 8229 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ω
∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o
∈ ω)) |
107 | 104, 105,
106 | sylanblrc 593 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) → ω ∈ (On
∖ 2o)) |
108 | 94 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) → 𝐶 ∈ On) |
109 | | simplr 769 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) → Lim 𝐶) |
110 | | oelimcl 8328 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ω
∈ (On ∖ 2o) ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → Lim (ω ↑o
𝐶)) |
111 | 107, 108,
109, 110 | syl12anc 837 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) → Lim (ω
↑o 𝐶)) |
112 | | oalim 8259 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ On ∧ ((ω
↑o 𝐶)
∈ On ∧ Lim (ω ↑o 𝐶))) → (𝐴 +o (ω ↑o
𝐶)) = ∪ 𝑦 ∈ (ω ↑o 𝐶)(𝐴 +o 𝑦)) |
113 | 102, 103,
111, 112 | syl12anc 837 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) → (𝐴 +o (ω ↑o
𝐶)) = ∪ 𝑦 ∈ (ω ↑o 𝐶)(𝐴 +o 𝑦)) |
114 | | oelim2 8323 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ω
∈ On ∧ (𝐶 ∈
On ∧ Lim 𝐶)) →
(ω ↑o 𝐶) = ∪
𝑧 ∈ (𝐶 ∖ 1o)(ω
↑o 𝑧)) |
115 | 93, 94, 95, 114 | syl12anc 837 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) → (ω
↑o 𝐶) =
∪ 𝑧 ∈ (𝐶 ∖ 1o)(ω
↑o 𝑧)) |
116 | 115 | eleq2d 2823 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) → (𝑦 ∈ (ω ↑o 𝐶) ↔ 𝑦 ∈ ∪
𝑧 ∈ (𝐶 ∖ 1o)(ω
↑o 𝑧))) |
117 | | eliun 4908 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ∪ 𝑧 ∈ (𝐶 ∖ 1o)(ω
↑o 𝑧)
↔ ∃𝑧 ∈
(𝐶 ∖
1o)𝑦 ∈
(ω ↑o 𝑧)) |
118 | 116, 117 | bitrdi 290 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) → (𝑦 ∈ (ω ↑o 𝐶) ↔ ∃𝑧 ∈ (𝐶 ∖ 1o)𝑦 ∈ (ω ↑o 𝑧))) |
119 | 118 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) → (𝑦 ∈ (ω ↑o 𝐶) ↔ ∃𝑧 ∈ (𝐶 ∖ 1o)𝑦 ∈ (ω ↑o 𝑧))) |
120 | | eldifi 4041 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ (𝐶 ∖ 1o) → 𝑧 ∈ 𝐶) |
121 | 104 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → ω ∈
On) |
122 | 108 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → 𝐶 ∈ On) |
123 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → 𝑥 ∈ 𝐶) |
124 | | onelon 6238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ On) |
125 | 122, 123,
124 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → 𝑥 ∈ On) |
126 | 121, 125,
46 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (ω
↑o 𝑥)
∈ On) |
127 | | eloni 6223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((ω
↑o 𝑥)
∈ On → Ord (ω ↑o 𝑥)) |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → Ord (ω
↑o 𝑥)) |
129 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → 𝐴 ∈ (ω ↑o 𝑥)) |
130 | | ordelss 6229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((Ord
(ω ↑o 𝑥) ∧ 𝐴 ∈ (ω ↑o 𝑥)) → 𝐴 ⊆ (ω ↑o 𝑥)) |
131 | 128, 129,
130 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → 𝐴 ⊆ (ω ↑o 𝑥)) |
132 | | ssun1 4086 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑥 ⊆ (𝑥 ∪ 𝑧) |
133 | 26 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → Ord 𝐶) |
134 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → 𝑧 ∈ 𝐶) |
135 | | ordunel 7606 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((Ord
𝐶 ∧ 𝑥 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶) → (𝑥 ∪ 𝑧) ∈ 𝐶) |
136 | 133, 123,
134, 135 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (𝑥 ∪ 𝑧) ∈ 𝐶) |
137 | | onelon 6238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐶 ∈ On ∧ (𝑥 ∪ 𝑧) ∈ 𝐶) → (𝑥 ∪ 𝑧) ∈ On) |
138 | 122, 136,
137 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (𝑥 ∪ 𝑧) ∈ On) |
139 | | peano1 7667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ∅
∈ ω |
140 | 139 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → ∅ ∈
ω) |
141 | | oewordi 8319 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 ∈ On ∧ (𝑥 ∪ 𝑧) ∈ On ∧ ω ∈ On) ∧
∅ ∈ ω) → (𝑥 ⊆ (𝑥 ∪ 𝑧) → (ω ↑o 𝑥) ⊆ (ω
↑o (𝑥 ∪
𝑧)))) |
142 | 125, 138,
121, 140, 141 | syl31anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (𝑥 ⊆ (𝑥 ∪ 𝑧) → (ω ↑o 𝑥) ⊆ (ω
↑o (𝑥 ∪
𝑧)))) |
143 | 132, 142 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (ω
↑o 𝑥)
⊆ (ω ↑o (𝑥 ∪ 𝑧))) |
144 | 131, 143 | sstrd 3911 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → 𝐴 ⊆ (ω ↑o (𝑥 ∪ 𝑧))) |
145 | 102 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → 𝐴 ∈ On) |
146 | | oecl 8264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((ω
∈ On ∧ (𝑥 ∪
𝑧) ∈ On) →
(ω ↑o (𝑥 ∪ 𝑧)) ∈ On) |
147 | 121, 138,
146 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (ω
↑o (𝑥 ∪
𝑧)) ∈
On) |
148 | | onelon 6238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐶 ∈ On ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ On) |
149 | 122, 134,
148 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → 𝑧 ∈ On) |
150 | | oecl 8264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((ω
∈ On ∧ 𝑧 ∈
On) → (ω ↑o 𝑧) ∈ On) |
151 | 121, 149,
150 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (ω
↑o 𝑧)
∈ On) |
152 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → 𝑦 ∈ (ω ↑o 𝑧)) |
153 | | onelon 6238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((ω ↑o 𝑧) ∈ On ∧ 𝑦 ∈ (ω ↑o 𝑧)) → 𝑦 ∈ On) |
154 | 151, 152,
153 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → 𝑦 ∈ On) |
155 | | oawordri 8278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ On ∧ (ω
↑o (𝑥 ∪
𝑧)) ∈ On ∧ 𝑦 ∈ On) → (𝐴 ⊆ (ω
↑o (𝑥 ∪
𝑧)) → (𝐴 +o 𝑦) ⊆ ((ω
↑o (𝑥 ∪
𝑧)) +o 𝑦))) |
156 | 145, 147,
154, 155 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (𝐴 ⊆ (ω ↑o (𝑥 ∪ 𝑧)) → (𝐴 +o 𝑦) ⊆ ((ω ↑o (𝑥 ∪ 𝑧)) +o 𝑦))) |
157 | 144, 156 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (𝐴 +o 𝑦) ⊆ ((ω ↑o (𝑥 ∪ 𝑧)) +o 𝑦)) |
158 | | eloni 6223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((ω
↑o 𝑧)
∈ On → Ord (ω ↑o 𝑧)) |
159 | 151, 158 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → Ord (ω
↑o 𝑧)) |
160 | | ordelss 6229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((Ord
(ω ↑o 𝑧) ∧ 𝑦 ∈ (ω ↑o 𝑧)) → 𝑦 ⊆ (ω ↑o 𝑧)) |
161 | 159, 152,
160 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → 𝑦 ⊆ (ω ↑o 𝑧)) |
162 | | ssun2 4087 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑧 ⊆ (𝑥 ∪ 𝑧) |
163 | | oewordi 8319 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑧 ∈ On ∧ (𝑥 ∪ 𝑧) ∈ On ∧ ω ∈ On) ∧
∅ ∈ ω) → (𝑧 ⊆ (𝑥 ∪ 𝑧) → (ω ↑o 𝑧) ⊆ (ω
↑o (𝑥 ∪
𝑧)))) |
164 | 149, 138,
121, 140, 163 | syl31anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (𝑧 ⊆ (𝑥 ∪ 𝑧) → (ω ↑o 𝑧) ⊆ (ω
↑o (𝑥 ∪
𝑧)))) |
165 | 162, 164 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (ω
↑o 𝑧)
⊆ (ω ↑o (𝑥 ∪ 𝑧))) |
166 | 161, 165 | sstrd 3911 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → 𝑦 ⊆ (ω ↑o (𝑥 ∪ 𝑧))) |
167 | | oaword 8277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ On ∧ (ω
↑o (𝑥 ∪
𝑧)) ∈ On ∧
(ω ↑o (𝑥 ∪ 𝑧)) ∈ On) → (𝑦 ⊆ (ω ↑o (𝑥 ∪ 𝑧)) ↔ ((ω ↑o (𝑥 ∪ 𝑧)) +o 𝑦) ⊆ ((ω ↑o (𝑥 ∪ 𝑧)) +o (ω ↑o
(𝑥 ∪ 𝑧))))) |
168 | 154, 147,
147, 167 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (𝑦 ⊆ (ω ↑o (𝑥 ∪ 𝑧)) ↔ ((ω ↑o (𝑥 ∪ 𝑧)) +o 𝑦) ⊆ ((ω ↑o (𝑥 ∪ 𝑧)) +o (ω ↑o
(𝑥 ∪ 𝑧))))) |
169 | 166, 168 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → ((ω
↑o (𝑥 ∪
𝑧)) +o 𝑦) ⊆ ((ω
↑o (𝑥 ∪
𝑧)) +o (ω
↑o (𝑥 ∪
𝑧)))) |
170 | 157, 169 | sstrd 3911 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (𝐴 +o 𝑦) ⊆ ((ω ↑o (𝑥 ∪ 𝑧)) +o (ω ↑o
(𝑥 ∪ 𝑧)))) |
171 | | ordom 7654 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ Ord
ω |
172 | | ordsucss 7597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (Ord
ω → (1o ∈ ω → suc 1o ⊆
ω)) |
173 | 171, 105,
172 | mp2 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ suc
1o ⊆ ω |
174 | | 1on 8209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
1o ∈ On |
175 | | suceloni 7592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(1o ∈ On → suc 1o ∈
On) |
176 | 174, 175 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → suc 1o
∈ On) |
177 | | omwordi 8299 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((suc
1o ∈ On ∧ ω ∈ On ∧ (ω
↑o (𝑥 ∪
𝑧)) ∈ On) → (suc
1o ⊆ ω → ((ω ↑o (𝑥 ∪ 𝑧)) ·o suc 1o)
⊆ ((ω ↑o (𝑥 ∪ 𝑧)) ·o
ω))) |
178 | 176, 121,
147, 177 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (suc 1o
⊆ ω → ((ω ↑o (𝑥 ∪ 𝑧)) ·o suc 1o)
⊆ ((ω ↑o (𝑥 ∪ 𝑧)) ·o
ω))) |
179 | 173, 178 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → ((ω
↑o (𝑥 ∪
𝑧)) ·o
suc 1o) ⊆ ((ω ↑o (𝑥 ∪ 𝑧)) ·o
ω)) |
180 | 174 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → 1o ∈
On) |
181 | | omsuc 8253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((ω ↑o (𝑥 ∪ 𝑧)) ∈ On ∧ 1o ∈ On)
→ ((ω ↑o (𝑥 ∪ 𝑧)) ·o suc 1o) =
(((ω ↑o (𝑥 ∪ 𝑧)) ·o 1o)
+o (ω ↑o (𝑥 ∪ 𝑧)))) |
182 | 147, 180,
181 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → ((ω
↑o (𝑥 ∪
𝑧)) ·o
suc 1o) = (((ω ↑o (𝑥 ∪ 𝑧)) ·o 1o)
+o (ω ↑o (𝑥 ∪ 𝑧)))) |
183 | | om1 8270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((ω
↑o (𝑥 ∪
𝑧)) ∈ On →
((ω ↑o (𝑥 ∪ 𝑧)) ·o 1o) =
(ω ↑o (𝑥 ∪ 𝑧))) |
184 | 147, 183 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → ((ω
↑o (𝑥 ∪
𝑧)) ·o
1o) = (ω ↑o (𝑥 ∪ 𝑧))) |
185 | 184 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (((ω
↑o (𝑥 ∪
𝑧)) ·o
1o) +o (ω ↑o (𝑥 ∪ 𝑧))) = ((ω ↑o (𝑥 ∪ 𝑧)) +o (ω ↑o
(𝑥 ∪ 𝑧)))) |
186 | 182, 185 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → ((ω
↑o (𝑥 ∪
𝑧)) +o (ω
↑o (𝑥 ∪
𝑧))) = ((ω
↑o (𝑥 ∪
𝑧)) ·o
suc 1o)) |
187 | | oesuc 8254 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((ω
∈ On ∧ (𝑥 ∪
𝑧) ∈ On) →
(ω ↑o suc (𝑥 ∪ 𝑧)) = ((ω ↑o (𝑥 ∪ 𝑧)) ·o
ω)) |
188 | 121, 138,
187 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (ω
↑o suc (𝑥
∪ 𝑧)) = ((ω
↑o (𝑥 ∪
𝑧)) ·o
ω)) |
189 | 179, 186,
188 | 3sstr4d 3948 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → ((ω
↑o (𝑥 ∪
𝑧)) +o (ω
↑o (𝑥 ∪
𝑧))) ⊆ (ω
↑o suc (𝑥
∪ 𝑧))) |
190 | 170, 189 | sstrd 3911 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (𝐴 +o 𝑦) ⊆ (ω ↑o suc
(𝑥 ∪ 𝑧))) |
191 | | ordsucss 7597 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Ord
𝐶 → ((𝑥 ∪ 𝑧) ∈ 𝐶 → suc (𝑥 ∪ 𝑧) ⊆ 𝐶)) |
192 | 133, 136,
191 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → suc (𝑥 ∪ 𝑧) ⊆ 𝐶) |
193 | | suceloni 7592 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∪ 𝑧) ∈ On → suc (𝑥 ∪ 𝑧) ∈ On) |
194 | 138, 193 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → suc (𝑥 ∪ 𝑧) ∈ On) |
195 | | oewordi 8319 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((suc
(𝑥 ∪ 𝑧) ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ On) ∧
∅ ∈ ω) → (suc (𝑥 ∪ 𝑧) ⊆ 𝐶 → (ω ↑o suc
(𝑥 ∪ 𝑧)) ⊆ (ω ↑o 𝐶))) |
196 | 194, 122,
121, 140, 195 | syl31anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (suc (𝑥 ∪ 𝑧) ⊆ 𝐶 → (ω ↑o suc
(𝑥 ∪ 𝑧)) ⊆ (ω ↑o 𝐶))) |
197 | 192, 196 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (ω
↑o suc (𝑥
∪ 𝑧)) ⊆ (ω
↑o 𝐶)) |
198 | 190, 197 | sstrd 3911 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑o 𝑧))) → (𝐴 +o 𝑦) ⊆ (ω ↑o 𝐶)) |
199 | 198 | expr 460 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ 𝑧 ∈ 𝐶) → (𝑦 ∈ (ω ↑o 𝑧) → (𝐴 +o 𝑦) ⊆ (ω ↑o 𝐶))) |
200 | 120, 199 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) ∧ 𝑧 ∈ (𝐶 ∖ 1o)) → (𝑦 ∈ (ω
↑o 𝑧)
→ (𝐴 +o
𝑦) ⊆ (ω
↑o 𝐶))) |
201 | 200 | rexlimdva 3203 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) → (∃𝑧 ∈ (𝐶 ∖ 1o)𝑦 ∈ (ω ↑o 𝑧) → (𝐴 +o 𝑦) ⊆ (ω ↑o 𝐶))) |
202 | 119, 201 | sylbid 243 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) → (𝑦 ∈ (ω ↑o 𝐶) → (𝐴 +o 𝑦) ⊆ (ω ↑o 𝐶))) |
203 | 202 | ralrimiv 3104 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) → ∀𝑦 ∈ (ω
↑o 𝐶)(𝐴 +o 𝑦) ⊆ (ω
↑o 𝐶)) |
204 | | iunss 4954 |
. . . . . . . . . . . . . . . . 17
⊢ (∪ 𝑦 ∈ (ω ↑o 𝐶)(𝐴 +o 𝑦) ⊆ (ω ↑o 𝐶) ↔ ∀𝑦 ∈ (ω
↑o 𝐶)(𝐴 +o 𝑦) ⊆ (ω
↑o 𝐶)) |
205 | 203, 204 | sylibr 237 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) → ∪ 𝑦 ∈ (ω ↑o 𝐶)(𝐴 +o 𝑦) ⊆ (ω ↑o 𝐶)) |
206 | 113, 205 | eqsstrd 3939 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑o 𝑥))) → (𝐴 +o (ω ↑o
𝐶)) ⊆ (ω
↑o 𝐶)) |
207 | 206 | expr 460 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ 𝑥 ∈ 𝐶) → (𝐴 ∈ (ω ↑o 𝑥) → (𝐴 +o (ω ↑o
𝐶)) ⊆ (ω
↑o 𝐶))) |
208 | 101, 207 | sylan2 596 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
(ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) ∧ 𝑥 ∈ (𝐶 ∖ 1o)) → (𝐴 ∈ (ω
↑o 𝑥)
→ (𝐴 +o
(ω ↑o 𝐶)) ⊆ (ω ↑o 𝐶))) |
209 | 208 | rexlimdva 3203 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) → (∃𝑥 ∈ (𝐶 ∖ 1o)𝐴 ∈ (ω ↑o 𝑥) → (𝐴 +o (ω ↑o
𝐶)) ⊆ (ω
↑o 𝐶))) |
210 | 100, 209 | mpd 15 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) → (𝐴 +o (ω ↑o
𝐶)) ⊆ (ω
↑o 𝐶)) |
211 | 88 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) → (ω
↑o 𝐶)
⊆ (𝐴 +o
(ω ↑o 𝐶))) |
212 | 210, 211 | eqssd 3918 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ Lim 𝐶) → (𝐴 +o (ω ↑o
𝐶)) = (ω
↑o 𝐶)) |
213 | 212 | ex 416 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) → (Lim
𝐶 → (𝐴 +o (ω ↑o
𝐶)) = (ω
↑o 𝐶))) |
214 | 43, 91, 213 | 3jaod 1430 |
. . . . . . . 8
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) → ((𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶) → (𝐴 +o (ω ↑o
𝐶)) = (ω
↑o 𝐶))) |
215 | 28, 214 | mpd 15 |
. . . . . . 7
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) → (𝐴 +o (ω
↑o 𝐶)) =
(ω ↑o 𝐶)) |
216 | 215 | adantr 484 |
. . . . . 6
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +o (ω
↑o 𝐶)) =
(ω ↑o 𝐶)) |
217 | 216 | oveq1d 7228 |
. . . . 5
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +o (ω
↑o 𝐶))
+o 𝑥) =
((ω ↑o 𝐶) +o 𝑥)) |
218 | 23, 217 | eqtr3d 2779 |
. . . 4
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +o ((ω
↑o 𝐶)
+o 𝑥)) =
((ω ↑o 𝐶) +o 𝑥)) |
219 | | oveq2 7221 |
. . . . 5
⊢
(((ω ↑o 𝐶) +o 𝑥) = 𝐵 → (𝐴 +o ((ω ↑o
𝐶) +o 𝑥)) = (𝐴 +o 𝐵)) |
220 | | id 22 |
. . . . 5
⊢
(((ω ↑o 𝐶) +o 𝑥) = 𝐵 → ((ω ↑o 𝐶) +o 𝑥) = 𝐵) |
221 | 219, 220 | eqeq12d 2753 |
. . . 4
⊢
(((ω ↑o 𝐶) +o 𝑥) = 𝐵 → ((𝐴 +o ((ω ↑o
𝐶) +o 𝑥)) = ((ω
↑o 𝐶)
+o 𝑥) ↔
(𝐴 +o 𝐵) = 𝐵)) |
222 | 218, 221 | syl5ibcom 248 |
. . 3
⊢ ((((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) ∧ 𝑥 ∈ On) → (((ω
↑o 𝐶)
+o 𝑥) = 𝐵 → (𝐴 +o 𝐵) = 𝐵)) |
223 | 222 | rexlimdva 3203 |
. 2
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) →
(∃𝑥 ∈ On
((ω ↑o 𝐶) +o 𝑥) = 𝐵 → (𝐴 +o 𝐵) = 𝐵)) |
224 | 15, 223 | mpd 15 |
1
⊢ (((𝐴 ∈ (ω
↑o 𝐶) ∧
𝐵 ∈ On) ∧ (ω
↑o 𝐶)
⊆ 𝐵) → (𝐴 +o 𝐵) = 𝐵) |