MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oaabs2 Structured version   Visualization version   GIF version

Theorem oaabs2 7900
Description: The absorption law oaabs 7899 is also a property of higher powers of ω. (Contributed by Mario Carneiro, 29-May-2015.)
Assertion
Ref Expression
oaabs2 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐴 +𝑜 𝐵) = 𝐵)

Proof of Theorem oaabs2
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 n0i 4078 . . . . . . 7 (𝐴 ∈ (ω ↑𝑜 𝐶) → ¬ (ω ↑𝑜 𝐶) = ∅)
2 fnoe 7765 . . . . . . . . 9 𝑜 Fn (On × On)
3 fndm 6141 . . . . . . . . 9 ( ↑𝑜 Fn (On × On) → dom ↑𝑜 = (On × On))
42, 3ax-mp 5 . . . . . . . 8 dom ↑𝑜 = (On × On)
54ndmov 6986 . . . . . . 7 (¬ (ω ∈ On ∧ 𝐶 ∈ On) → (ω ↑𝑜 𝐶) = ∅)
61, 5nsyl2 144 . . . . . 6 (𝐴 ∈ (ω ↑𝑜 𝐶) → (ω ∈ On ∧ 𝐶 ∈ On))
76ad2antrr 706 . . . . 5 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ∈ On ∧ 𝐶 ∈ On))
8 oecl 7792 . . . . 5 ((ω ∈ On ∧ 𝐶 ∈ On) → (ω ↑𝑜 𝐶) ∈ On)
97, 8syl 17 . . . 4 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜 𝐶) ∈ On)
10 simplr 774 . . . 4 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → 𝐵 ∈ On)
11 simpr 472 . . . 4 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜 𝐶) ⊆ 𝐵)
12 oawordeu 7810 . . . 4 ((((ω ↑𝑜 𝐶) ∈ On ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ∃!𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
139, 10, 11, 12syl21anc 855 . . 3 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ∃!𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
14 reurex 3313 . . 3 (∃!𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → ∃𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
1513, 14syl 17 . 2 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ∃𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
16 simpll 772 . . . . . . . 8 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → 𝐴 ∈ (ω ↑𝑜 𝐶))
17 onelon 5902 . . . . . . . 8 (((ω ↑𝑜 𝐶) ∈ On ∧ 𝐴 ∈ (ω ↑𝑜 𝐶)) → 𝐴 ∈ On)
189, 16, 17syl2anc 574 . . . . . . 7 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → 𝐴 ∈ On)
1918adantr 467 . . . . . 6 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝐴 ∈ On)
209adantr 467 . . . . . 6 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (ω ↑𝑜 𝐶) ∈ On)
21 simpr 472 . . . . . 6 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝑥 ∈ On)
22 oaass 7816 . . . . . 6 ((𝐴 ∈ On ∧ (ω ↑𝑜 𝐶) ∈ On ∧ 𝑥 ∈ On) → ((𝐴 +𝑜 (ω ↑𝑜 𝐶)) +𝑜 𝑥) = (𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)))
2319, 20, 21, 22syl3anc 1480 . . . . 5 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +𝑜 (ω ↑𝑜 𝐶)) +𝑜 𝑥) = (𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)))
247simprd 484 . . . . . . . . . 10 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → 𝐶 ∈ On)
25 eloni 5887 . . . . . . . . . 10 (𝐶 ∈ On → Ord 𝐶)
2624, 25syl 17 . . . . . . . . 9 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → Ord 𝐶)
27 ordzsl 7213 . . . . . . . . 9 (Ord 𝐶 ↔ (𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶))
2826, 27sylib 209 . . . . . . . 8 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶))
29 simplll 780 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 ∈ (ω ↑𝑜 𝐶))
30 oveq2 6820 . . . . . . . . . . . . . . 15 (𝐶 = ∅ → (ω ↑𝑜 𝐶) = (ω ↑𝑜 ∅))
317simpld 483 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ω ∈ On)
32 oe0 7777 . . . . . . . . . . . . . . . 16 (ω ∈ On → (ω ↑𝑜 ∅) = 1𝑜)
3331, 32syl 17 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜 ∅) = 1𝑜)
3430, 33sylan9eqr 2830 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (ω ↑𝑜 𝐶) = 1𝑜)
3529, 34eleqtrd 2855 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 ∈ 1𝑜)
36 el1o 7754 . . . . . . . . . . . . 13 (𝐴 ∈ 1𝑜𝐴 = ∅)
3735, 36sylib 209 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 = ∅)
3837oveq1d 6827 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (∅ +𝑜 (ω ↑𝑜 𝐶)))
399adantr 467 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (ω ↑𝑜 𝐶) ∈ On)
40 oa0r 7793 . . . . . . . . . . . 12 ((ω ↑𝑜 𝐶) ∈ On → (∅ +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
4139, 40syl 17 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (∅ +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
4238, 41eqtrd 2808 . . . . . . . . . 10 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
4342ex 398 . . . . . . . . 9 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐶 = ∅ → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶)))
4431adantr 467 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → ω ∈ On)
45 simprl 776 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝑥 ∈ On)
46 oecl 7792 . . . . . . . . . . . . . 14 ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑𝑜 𝑥) ∈ On)
4744, 45, 46syl2anc 574 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 𝑥) ∈ On)
48 limom 7248 . . . . . . . . . . . . . 14 Lim ω
4944, 48jctir 511 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ∈ On ∧ Lim ω))
50 simplll 780 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐴 ∈ (ω ↑𝑜 𝐶))
51 simprr 778 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐶 = suc 𝑥)
5251oveq2d 6828 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 𝐶) = (ω ↑𝑜 suc 𝑥))
53 oesuc 7782 . . . . . . . . . . . . . . . 16 ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑𝑜 suc 𝑥) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
5444, 45, 53syl2anc 574 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 suc 𝑥) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
5552, 54eqtrd 2808 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 𝐶) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
5650, 55eleqtrd 2855 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 ω))
57 omordlim 7832 . . . . . . . . . . . . 13 ((((ω ↑𝑜 𝑥) ∈ On ∧ (ω ∈ On ∧ Lim ω)) ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 ω)) → ∃𝑦 ∈ ω 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
5847, 49, 56, 57syl21anc 855 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → ∃𝑦 ∈ ω 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
5947adantr 467 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (ω ↑𝑜 𝑥) ∈ On)
60 nnon 7239 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ω → 𝑦 ∈ On)
6160ad2antrl 708 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝑦 ∈ On)
62 omcl 7791 . . . . . . . . . . . . . . . . 17 (((ω ↑𝑜 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∈ On)
6359, 61, 62syl2anc 574 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → ((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∈ On)
64 eloni 5887 . . . . . . . . . . . . . . . 16 (((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∈ On → Ord ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
6563, 64syl 17 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → Ord ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
66 simprr 778 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
67 ordelss 5893 . . . . . . . . . . . . . . 15 ((Ord ((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦)) → 𝐴 ⊆ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
6865, 66, 67syl2anc 574 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝐴 ⊆ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
6918ad2antrr 706 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝐴 ∈ On)
709ad2antrr 706 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (ω ↑𝑜 𝐶) ∈ On)
71 oawordri 7805 . . . . . . . . . . . . . . 15 ((𝐴 ∈ On ∧ ((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∈ On ∧ (ω ↑𝑜 𝐶) ∈ On) → (𝐴 ⊆ ((ω ↑𝑜 𝑥) ·𝑜 𝑦) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶))))
7269, 63, 70, 71syl3anc 1480 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (𝐴 ⊆ ((ω ↑𝑜 𝑥) ·𝑜 𝑦) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶))))
7368, 72mpd 15 . . . . . . . . . . . . 13 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶)))
7444adantr 467 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → ω ∈ On)
75 odi 7834 . . . . . . . . . . . . . . . 16 (((ω ↑𝑜 𝑥) ∈ On ∧ 𝑦 ∈ On ∧ ω ∈ On) → ((ω ↑𝑜 𝑥) ·𝑜 (𝑦 +𝑜 ω)) = (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 ((ω ↑𝑜 𝑥) ·𝑜 ω)))
7659, 61, 74, 75syl3anc 1480 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → ((ω ↑𝑜 𝑥) ·𝑜 (𝑦 +𝑜 ω)) = (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 ((ω ↑𝑜 𝑥) ·𝑜 ω)))
77 simprl 776 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝑦 ∈ ω)
78 oaabslem 7898 . . . . . . . . . . . . . . . . 17 ((ω ∈ On ∧ 𝑦 ∈ ω) → (𝑦 +𝑜 ω) = ω)
7974, 77, 78syl2anc 574 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (𝑦 +𝑜 ω) = ω)
8079oveq2d 6828 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → ((ω ↑𝑜 𝑥) ·𝑜 (𝑦 +𝑜 ω)) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
8176, 80eqtr3d 2810 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 ((ω ↑𝑜 𝑥) ·𝑜 ω)) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
8255adantr 467 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (ω ↑𝑜 𝐶) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
8382oveq2d 6828 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶)) = (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 ((ω ↑𝑜 𝑥) ·𝑜 ω)))
8481, 83, 823eqtr4d 2818 . . . . . . . . . . . . 13 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
8573, 84sseqtrd 3797 . . . . . . . . . . . 12 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶))
8658, 85rexlimddv 3187 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶))
87 oaword2 7808 . . . . . . . . . . . . 13 (((ω ↑𝑜 𝐶) ∈ On ∧ 𝐴 ∈ On) → (ω ↑𝑜 𝐶) ⊆ (𝐴 +𝑜 (ω ↑𝑜 𝐶)))
889, 18, 87syl2anc 574 . . . . . . . . . . . 12 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜 𝐶) ⊆ (𝐴 +𝑜 (ω ↑𝑜 𝐶)))
8988adantr 467 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 𝐶) ⊆ (𝐴 +𝑜 (ω ↑𝑜 𝐶)))
9086, 89eqssd 3775 . . . . . . . . . 10 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
9190rexlimdvaa 3184 . . . . . . . . 9 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (∃𝑥 ∈ On 𝐶 = suc 𝑥 → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶)))
92 simplll 780 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐴 ∈ (ω ↑𝑜 𝐶))
9331adantr 467 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → ω ∈ On)
9424adantr 467 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐶 ∈ On)
95 simpr 472 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → Lim 𝐶)
96 oelim2 7850 . . . . . . . . . . . . . . 15 ((ω ∈ On ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → (ω ↑𝑜 𝐶) = 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑥))
9793, 94, 95, 96syl12anc 854 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑𝑜 𝐶) = 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑥))
9892, 97eleqtrd 2855 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐴 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑥))
99 eliun 4669 . . . . . . . . . . . . 13 (𝐴 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑥) ↔ ∃𝑥 ∈ (𝐶 ∖ 1𝑜)𝐴 ∈ (ω ↑𝑜 𝑥))
10098, 99sylib 209 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → ∃𝑥 ∈ (𝐶 ∖ 1𝑜)𝐴 ∈ (ω ↑𝑜 𝑥))
101 eldifi 3890 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐶 ∖ 1𝑜) → 𝑥𝐶)
10218ad2antrr 706 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → 𝐴 ∈ On)
1039ad2antrr 706 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (ω ↑𝑜 𝐶) ∈ On)
10493adantr 467 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → ω ∈ On)
105 1onn 7894 . . . . . . . . . . . . . . . . . . . 20 1𝑜 ∈ ω
106105a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → 1𝑜 ∈ ω)
107 ondif2 7757 . . . . . . . . . . . . . . . . . . 19 (ω ∈ (On ∖ 2𝑜) ↔ (ω ∈ On ∧ 1𝑜 ∈ ω))
108104, 106, 107sylanbrc 573 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → ω ∈ (On ∖ 2𝑜))
10994adantr 467 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → 𝐶 ∈ On)
110 simplr 774 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → Lim 𝐶)
111 oelimcl 7855 . . . . . . . . . . . . . . . . . 18 ((ω ∈ (On ∖ 2𝑜) ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → Lim (ω ↑𝑜 𝐶))
112108, 109, 110, 111syl12anc 854 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → Lim (ω ↑𝑜 𝐶))
113 oalim 7787 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ ((ω ↑𝑜 𝐶) ∈ On ∧ Lim (ω ↑𝑜 𝐶))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = 𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦))
114102, 103, 112, 113syl12anc 854 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = 𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦))
115 oelim2 7850 . . . . . . . . . . . . . . . . . . . . . . 23 ((ω ∈ On ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → (ω ↑𝑜 𝐶) = 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑧))
11693, 94, 95, 115syl12anc 854 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑𝑜 𝐶) = 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑧))
117116eleq2d 2839 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝑦 ∈ (ω ↑𝑜 𝐶) ↔ 𝑦 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑧)))
118 eliun 4669 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑧) ↔ ∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω ↑𝑜 𝑧))
119117, 118syl6bb 277 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝑦 ∈ (ω ↑𝑜 𝐶) ↔ ∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω ↑𝑜 𝑧)))
120119adantr 467 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (𝑦 ∈ (ω ↑𝑜 𝐶) ↔ ∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω ↑𝑜 𝑧)))
121 eldifi 3890 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ (𝐶 ∖ 1𝑜) → 𝑧𝐶)
122104adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ω ∈ On)
123109adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐶 ∈ On)
124 simplrl 784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑥𝐶)
125 onelon 5902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐶 ∈ On ∧ 𝑥𝐶) → 𝑥 ∈ On)
126123, 124, 125syl2anc 574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑥 ∈ On)
127122, 126, 46syl2anc 574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 𝑥) ∈ On)
128 eloni 5887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ω ↑𝑜 𝑥) ∈ On → Ord (ω ↑𝑜 𝑥))
129127, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → Ord (ω ↑𝑜 𝑥))
130 simplrr 785 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐴 ∈ (ω ↑𝑜 𝑥))
131 ordelss 5893 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Ord (ω ↑𝑜 𝑥) ∧ 𝐴 ∈ (ω ↑𝑜 𝑥)) → 𝐴 ⊆ (ω ↑𝑜 𝑥))
132129, 130, 131syl2anc 574 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐴 ⊆ (ω ↑𝑜 𝑥))
133 ssun1 3934 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑥 ⊆ (𝑥𝑧)
13426ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → Ord 𝐶)
135 simprl 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑧𝐶)
136 ordunel 7195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((Ord 𝐶𝑥𝐶𝑧𝐶) → (𝑥𝑧) ∈ 𝐶)
137134, 124, 135, 136syl3anc 1480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑥𝑧) ∈ 𝐶)
138 onelon 5902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐶 ∈ On ∧ (𝑥𝑧) ∈ 𝐶) → (𝑥𝑧) ∈ On)
139123, 137, 138syl2anc 574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑥𝑧) ∈ On)
140 peano1 7253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ ∈ ω
141140a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ∅ ∈ ω)
142 oewordi 7846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 ∈ On ∧ (𝑥𝑧) ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (𝑥 ⊆ (𝑥𝑧) → (ω ↑𝑜 𝑥) ⊆ (ω ↑𝑜 (𝑥𝑧))))
143126, 139, 122, 141, 142syl31anc 1482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑥 ⊆ (𝑥𝑧) → (ω ↑𝑜 𝑥) ⊆ (ω ↑𝑜 (𝑥𝑧))))
144133, 143mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 𝑥) ⊆ (ω ↑𝑜 (𝑥𝑧)))
145132, 144sstrd 3768 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐴 ⊆ (ω ↑𝑜 (𝑥𝑧)))
146102adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐴 ∈ On)
147 oecl 7792 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ω ∈ On ∧ (𝑥𝑧) ∈ On) → (ω ↑𝑜 (𝑥𝑧)) ∈ On)
148122, 139, 147syl2anc 574 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 (𝑥𝑧)) ∈ On)
149 onelon 5902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐶 ∈ On ∧ 𝑧𝐶) → 𝑧 ∈ On)
150123, 135, 149syl2anc 574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑧 ∈ On)
151 oecl 7792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ω ∈ On ∧ 𝑧 ∈ On) → (ω ↑𝑜 𝑧) ∈ On)
152122, 150, 151syl2anc 574 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 𝑧) ∈ On)
153 simprr 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑦 ∈ (ω ↑𝑜 𝑧))
154 onelon 5902 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ω ↑𝑜 𝑧) ∈ On ∧ 𝑦 ∈ (ω ↑𝑜 𝑧)) → 𝑦 ∈ On)
155152, 153, 154syl2anc 574 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑦 ∈ On)
156 oawordri 7805 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ On ∧ (ω ↑𝑜 (𝑥𝑧)) ∈ On ∧ 𝑦 ∈ On) → (𝐴 ⊆ (ω ↑𝑜 (𝑥𝑧)) → (𝐴 +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦)))
157146, 148, 155, 156syl3anc 1480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 ⊆ (ω ↑𝑜 (𝑥𝑧)) → (𝐴 +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦)))
158145, 157mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦))
159 eloni 5887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ω ↑𝑜 𝑧) ∈ On → Ord (ω ↑𝑜 𝑧))
160152, 159syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → Ord (ω ↑𝑜 𝑧))
161 ordelss 5893 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Ord (ω ↑𝑜 𝑧) ∧ 𝑦 ∈ (ω ↑𝑜 𝑧)) → 𝑦 ⊆ (ω ↑𝑜 𝑧))
162160, 153, 161syl2anc 574 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑦 ⊆ (ω ↑𝑜 𝑧))
163 ssun2 3935 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑧 ⊆ (𝑥𝑧)
164 oewordi 7846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑧 ∈ On ∧ (𝑥𝑧) ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (𝑧 ⊆ (𝑥𝑧) → (ω ↑𝑜 𝑧) ⊆ (ω ↑𝑜 (𝑥𝑧))))
165150, 139, 122, 141, 164syl31anc 1482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑧 ⊆ (𝑥𝑧) → (ω ↑𝑜 𝑧) ⊆ (ω ↑𝑜 (𝑥𝑧))))
166163, 165mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 𝑧) ⊆ (ω ↑𝑜 (𝑥𝑧)))
167162, 166sstrd 3768 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑦 ⊆ (ω ↑𝑜 (𝑥𝑧)))
168 oaword 7804 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ On ∧ (ω ↑𝑜 (𝑥𝑧)) ∈ On ∧ (ω ↑𝑜 (𝑥𝑧)) ∈ On) → (𝑦 ⊆ (ω ↑𝑜 (𝑥𝑧)) ↔ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧)))))
169155, 148, 148, 168syl3anc 1480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑦 ⊆ (ω ↑𝑜 (𝑥𝑧)) ↔ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧)))))
170167, 169mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
171158, 170sstrd 3768 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
172 ordom 7242 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ord ω
173 ordsucss 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Ord ω → (1𝑜 ∈ ω → suc 1𝑜 ⊆ ω))
174172, 105, 173mp2 9 . . . . . . . . . . . . . . . . . . . . . . . . . 26 suc 1𝑜 ⊆ ω
175 1on 7741 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1𝑜 ∈ On
176 suceloni 7181 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1𝑜 ∈ On → suc 1𝑜 ∈ On)
177175, 176mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → suc 1𝑜 ∈ On)
178 omwordi 7826 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((suc 1𝑜 ∈ On ∧ ω ∈ On ∧ (ω ↑𝑜 (𝑥𝑧)) ∈ On) → (suc 1𝑜 ⊆ ω → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) ⊆ ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω)))
179177, 122, 148, 178syl3anc 1480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (suc 1𝑜 ⊆ ω → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) ⊆ ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω)))
180174, 179mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) ⊆ ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω))
181175a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 1𝑜 ∈ On)
182 omsuc 7781 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((ω ↑𝑜 (𝑥𝑧)) ∈ On ∧ 1𝑜 ∈ On) → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) = (((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
183148, 181, 182syl2anc 574 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) = (((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
184 om1 7797 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ω ↑𝑜 (𝑥𝑧)) ∈ On → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) = (ω ↑𝑜 (𝑥𝑧)))
185148, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) = (ω ↑𝑜 (𝑥𝑧)))
186185oveq1d 6827 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) +𝑜 (ω ↑𝑜 (𝑥𝑧))) = ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
187183, 186eqtr2d 2809 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))) = ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜))
188 oesuc 7782 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ω ∈ On ∧ (𝑥𝑧) ∈ On) → (ω ↑𝑜 suc (𝑥𝑧)) = ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω))
189122, 139, 188syl2anc 574 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 suc (𝑥𝑧)) = ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω))
190180, 187, 1893sstr4d 3804 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))) ⊆ (ω ↑𝑜 suc (𝑥𝑧)))
191171, 190sstrd 3768 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 suc (𝑥𝑧)))
192 ordsucss 7186 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord 𝐶 → ((𝑥𝑧) ∈ 𝐶 → suc (𝑥𝑧) ⊆ 𝐶))
193134, 137, 192sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → suc (𝑥𝑧) ⊆ 𝐶)
194 suceloni 7181 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥𝑧) ∈ On → suc (𝑥𝑧) ∈ On)
195139, 194syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → suc (𝑥𝑧) ∈ On)
196 oewordi 7846 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((suc (𝑥𝑧) ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (suc (𝑥𝑧) ⊆ 𝐶 → (ω ↑𝑜 suc (𝑥𝑧)) ⊆ (ω ↑𝑜 𝐶)))
197195, 123, 122, 141, 196syl31anc 1482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (suc (𝑥𝑧) ⊆ 𝐶 → (ω ↑𝑜 suc (𝑥𝑧)) ⊆ (ω ↑𝑜 𝐶)))
198193, 197mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 suc (𝑥𝑧)) ⊆ (ω ↑𝑜 𝐶))
199191, 198sstrd 3768 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶))
200199expr 445 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ 𝑧𝐶) → (𝑦 ∈ (ω ↑𝑜 𝑧) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶)))
201121, 200sylan2 581 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ 𝑧 ∈ (𝐶 ∖ 1𝑜)) → (𝑦 ∈ (ω ↑𝑜 𝑧) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶)))
202201rexlimdva 3183 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω ↑𝑜 𝑧) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶)))
203120, 202sylbid 231 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (𝑦 ∈ (ω ↑𝑜 𝐶) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶)))
204203ralrimiv 3117 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → ∀𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶))
205 iunss 4706 . . . . . . . . . . . . . . . . 17 ( 𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶) ↔ ∀𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶))
206204, 205sylibr 225 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → 𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶))
207114, 206eqsstrd 3795 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶))
208207expr 445 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ 𝑥𝐶) → (𝐴 ∈ (ω ↑𝑜 𝑥) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶)))
209101, 208sylan2 581 . . . . . . . . . . . . 13 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ 𝑥 ∈ (𝐶 ∖ 1𝑜)) → (𝐴 ∈ (ω ↑𝑜 𝑥) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶)))
210209rexlimdva 3183 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (∃𝑥 ∈ (𝐶 ∖ 1𝑜)𝐴 ∈ (ω ↑𝑜 𝑥) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶)))
211100, 210mpd 15 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶))
21288adantr 467 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑𝑜 𝐶) ⊆ (𝐴 +𝑜 (ω ↑𝑜 𝐶)))
213211, 212eqssd 3775 . . . . . . . . . 10 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
214213ex 398 . . . . . . . . 9 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (Lim 𝐶 → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶)))
21543, 91, 2143jaod 1543 . . . . . . . 8 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ((𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶)))
21628, 215mpd 15 . . . . . . 7 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
217216adantr 467 . . . . . 6 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
218217oveq1d 6827 . . . . 5 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +𝑜 (ω ↑𝑜 𝐶)) +𝑜 𝑥) = ((ω ↑𝑜 𝐶) +𝑜 𝑥))
21923, 218eqtr3d 2810 . . . 4 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)) = ((ω ↑𝑜 𝐶) +𝑜 𝑥))
220 oveq2 6820 . . . . 5 (((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → (𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)) = (𝐴 +𝑜 𝐵))
221 id 22 . . . . 5 (((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
222220, 221eqeq12d 2789 . . . 4 (((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → ((𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)) = ((ω ↑𝑜 𝐶) +𝑜 𝑥) ↔ (𝐴 +𝑜 𝐵) = 𝐵))
223219, 222syl5ibcom 236 . . 3 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → (𝐴 +𝑜 𝐵) = 𝐵))
224223rexlimdva 3183 . 2 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (∃𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → (𝐴 +𝑜 𝐵) = 𝐵))
22515, 224mpd 15 1 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐴 +𝑜 𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 383  w3o 1097   = wceq 1634  wcel 2148  wral 3064  wrex 3065  ∃!wreu 3066  cdif 3726  cun 3727  wss 3729  c0 4073   ciun 4665   × cxp 5261  dom cdm 5263  Ord word 5876  Oncon0 5877  Lim wlim 5878  suc csuc 5879   Fn wfn 6037  (class class class)co 6812  ωcom 7233  1𝑜c1o 7727  2𝑜c2o 7728   +𝑜 coa 7731   ·𝑜 comu 7732  𝑜 coe 7733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-rep 4917  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-pss 3745  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-tp 4331  df-op 4333  df-uni 4586  df-int 4623  df-iun 4667  df-br 4798  df-opab 4860  df-mpt 4877  df-tr 4900  df-id 5171  df-eprel 5176  df-po 5184  df-so 5185  df-fr 5222  df-we 5224  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-pred 5834  df-ord 5880  df-on 5881  df-lim 5882  df-suc 5883  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-om 7234  df-1st 7336  df-2nd 7337  df-wrecs 7580  df-recs 7642  df-rdg 7680  df-1o 7734  df-2o 7735  df-oadd 7738  df-omul 7739  df-oexp 7740
This theorem is referenced by:  cnfcomlem  8781
  Copyright terms: Public domain W3C validator