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

Theorem oaabs2 7890
Description: The absorption law oaabs 7889 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 4059 . . . . . . 7 (𝐴 ∈ (ω ↑𝑜 𝐶) → ¬ (ω ↑𝑜 𝐶) = ∅)
2 fnoe 7755 . . . . . . . . 9 𝑜 Fn (On × On)
3 fndm 6147 . . . . . . . . 9 ( ↑𝑜 Fn (On × On) → dom ↑𝑜 = (On × On))
42, 3ax-mp 5 . . . . . . . 8 dom ↑𝑜 = (On × On)
54ndmov 6979 . . . . . . 7 (¬ (ω ∈ On ∧ 𝐶 ∈ On) → (ω ↑𝑜 𝐶) = ∅)
61, 5nsyl2 142 . . . . . 6 (𝐴 ∈ (ω ↑𝑜 𝐶) → (ω ∈ On ∧ 𝐶 ∈ On))
76ad2antrr 764 . . . . 5 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ∈ On ∧ 𝐶 ∈ On))
8 oecl 7782 . . . . 5 ((ω ∈ On ∧ 𝐶 ∈ On) → (ω ↑𝑜 𝐶) ∈ On)
97, 8syl 17 . . . 4 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜 𝐶) ∈ On)
10 simplr 809 . . . 4 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → 𝐵 ∈ On)
11 simpr 479 . . . 4 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜 𝐶) ⊆ 𝐵)
12 oawordeu 7800 . . . 4 ((((ω ↑𝑜 𝐶) ∈ On ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ∃!𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
139, 10, 11, 12syl21anc 1476 . . 3 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ∃!𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
14 reurex 3295 . . 3 (∃!𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → ∃𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
1513, 14syl 17 . 2 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ∃𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
16 simpll 807 . . . . . . . 8 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → 𝐴 ∈ (ω ↑𝑜 𝐶))
17 onelon 5905 . . . . . . . 8 (((ω ↑𝑜 𝐶) ∈ On ∧ 𝐴 ∈ (ω ↑𝑜 𝐶)) → 𝐴 ∈ On)
189, 16, 17syl2anc 696 . . . . . . 7 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → 𝐴 ∈ On)
1918adantr 472 . . . . . 6 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝐴 ∈ On)
209adantr 472 . . . . . 6 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (ω ↑𝑜 𝐶) ∈ On)
21 simpr 479 . . . . . 6 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝑥 ∈ On)
22 oaass 7806 . . . . . 6 ((𝐴 ∈ On ∧ (ω ↑𝑜 𝐶) ∈ On ∧ 𝑥 ∈ On) → ((𝐴 +𝑜 (ω ↑𝑜 𝐶)) +𝑜 𝑥) = (𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)))
2319, 20, 21, 22syl3anc 1477 . . . . 5 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +𝑜 (ω ↑𝑜 𝐶)) +𝑜 𝑥) = (𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)))
247simprd 482 . . . . . . . . . 10 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → 𝐶 ∈ On)
25 eloni 5890 . . . . . . . . . 10 (𝐶 ∈ On → Ord 𝐶)
2624, 25syl 17 . . . . . . . . 9 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → Ord 𝐶)
27 ordzsl 7206 . . . . . . . . 9 (Ord 𝐶 ↔ (𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶))
2826, 27sylib 208 . . . . . . . 8 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶))
29 simplll 815 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 ∈ (ω ↑𝑜 𝐶))
30 oveq2 6817 . . . . . . . . . . . . . . 15 (𝐶 = ∅ → (ω ↑𝑜 𝐶) = (ω ↑𝑜 ∅))
317simpld 477 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ω ∈ On)
32 oe0 7767 . . . . . . . . . . . . . . . 16 (ω ∈ On → (ω ↑𝑜 ∅) = 1𝑜)
3331, 32syl 17 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜 ∅) = 1𝑜)
3430, 33sylan9eqr 2812 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (ω ↑𝑜 𝐶) = 1𝑜)
3529, 34eleqtrd 2837 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 ∈ 1𝑜)
36 el1o 7744 . . . . . . . . . . . . 13 (𝐴 ∈ 1𝑜𝐴 = ∅)
3735, 36sylib 208 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 = ∅)
3837oveq1d 6824 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (∅ +𝑜 (ω ↑𝑜 𝐶)))
399adantr 472 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (ω ↑𝑜 𝐶) ∈ On)
40 oa0r 7783 . . . . . . . . . . . 12 ((ω ↑𝑜 𝐶) ∈ On → (∅ +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
4139, 40syl 17 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (∅ +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
4238, 41eqtrd 2790 . . . . . . . . . 10 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
4342ex 449 . . . . . . . . 9 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐶 = ∅ → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶)))
4431adantr 472 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → ω ∈ On)
45 simprl 811 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝑥 ∈ On)
46 oecl 7782 . . . . . . . . . . . . . 14 ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑𝑜 𝑥) ∈ On)
4744, 45, 46syl2anc 696 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 𝑥) ∈ On)
48 limom 7241 . . . . . . . . . . . . . 14 Lim ω
4944, 48jctir 562 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ∈ On ∧ Lim ω))
50 simplll 815 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐴 ∈ (ω ↑𝑜 𝐶))
51 simprr 813 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐶 = suc 𝑥)
5251oveq2d 6825 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 𝐶) = (ω ↑𝑜 suc 𝑥))
53 oesuc 7772 . . . . . . . . . . . . . . . 16 ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑𝑜 suc 𝑥) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
5444, 45, 53syl2anc 696 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 suc 𝑥) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
5552, 54eqtrd 2790 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 𝐶) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
5650, 55eleqtrd 2837 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 ω))
57 omordlim 7822 . . . . . . . . . . . . 13 ((((ω ↑𝑜 𝑥) ∈ On ∧ (ω ∈ On ∧ Lim ω)) ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 ω)) → ∃𝑦 ∈ ω 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
5847, 49, 56, 57syl21anc 1476 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → ∃𝑦 ∈ ω 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
5947adantr 472 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (ω ↑𝑜 𝑥) ∈ On)
60 nnon 7232 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ω → 𝑦 ∈ On)
6160ad2antrl 766 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝑦 ∈ On)
62 omcl 7781 . . . . . . . . . . . . . . . . 17 (((ω ↑𝑜 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∈ On)
6359, 61, 62syl2anc 696 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → ((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∈ On)
64 eloni 5890 . . . . . . . . . . . . . . . 16 (((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∈ On → Ord ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
6563, 64syl 17 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → Ord ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
66 simprr 813 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
67 ordelss 5896 . . . . . . . . . . . . . . 15 ((Ord ((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦)) → 𝐴 ⊆ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
6865, 66, 67syl2anc 696 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝐴 ⊆ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
6918ad2antrr 764 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝐴 ∈ On)
709ad2antrr 764 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (ω ↑𝑜 𝐶) ∈ On)
71 oawordri 7795 . . . . . . . . . . . . . . 15 ((𝐴 ∈ On ∧ ((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∈ On ∧ (ω ↑𝑜 𝐶) ∈ On) → (𝐴 ⊆ ((ω ↑𝑜 𝑥) ·𝑜 𝑦) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶))))
7269, 63, 70, 71syl3anc 1477 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (𝐴 ⊆ ((ω ↑𝑜 𝑥) ·𝑜 𝑦) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶))))
7368, 72mpd 15 . . . . . . . . . . . . 13 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶)))
7444adantr 472 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → ω ∈ On)
75 odi 7824 . . . . . . . . . . . . . . . 16 (((ω ↑𝑜 𝑥) ∈ On ∧ 𝑦 ∈ On ∧ ω ∈ On) → ((ω ↑𝑜 𝑥) ·𝑜 (𝑦 +𝑜 ω)) = (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 ((ω ↑𝑜 𝑥) ·𝑜 ω)))
7659, 61, 74, 75syl3anc 1477 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → ((ω ↑𝑜 𝑥) ·𝑜 (𝑦 +𝑜 ω)) = (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 ((ω ↑𝑜 𝑥) ·𝑜 ω)))
77 simprl 811 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝑦 ∈ ω)
78 oaabslem 7888 . . . . . . . . . . . . . . . . 17 ((ω ∈ On ∧ 𝑦 ∈ ω) → (𝑦 +𝑜 ω) = ω)
7974, 77, 78syl2anc 696 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (𝑦 +𝑜 ω) = ω)
8079oveq2d 6825 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → ((ω ↑𝑜 𝑥) ·𝑜 (𝑦 +𝑜 ω)) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
8176, 80eqtr3d 2792 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 ((ω ↑𝑜 𝑥) ·𝑜 ω)) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
8255adantr 472 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (ω ↑𝑜 𝐶) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
8382oveq2d 6825 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶)) = (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 ((ω ↑𝑜 𝑥) ·𝑜 ω)))
8481, 83, 823eqtr4d 2800 . . . . . . . . . . . . 13 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
8573, 84sseqtrd 3778 . . . . . . . . . . . 12 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶))
8658, 85rexlimddv 3169 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶))
87 oaword2 7798 . . . . . . . . . . . . 13 (((ω ↑𝑜 𝐶) ∈ On ∧ 𝐴 ∈ On) → (ω ↑𝑜 𝐶) ⊆ (𝐴 +𝑜 (ω ↑𝑜 𝐶)))
889, 18, 87syl2anc 696 . . . . . . . . . . . 12 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜 𝐶) ⊆ (𝐴 +𝑜 (ω ↑𝑜 𝐶)))
8988adantr 472 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 𝐶) ⊆ (𝐴 +𝑜 (ω ↑𝑜 𝐶)))
9086, 89eqssd 3757 . . . . . . . . . 10 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
9190rexlimdvaa 3166 . . . . . . . . 9 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (∃𝑥 ∈ On 𝐶 = suc 𝑥 → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶)))
92 simplll 815 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐴 ∈ (ω ↑𝑜 𝐶))
9331adantr 472 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → ω ∈ On)
9424adantr 472 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐶 ∈ On)
95 simpr 479 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → Lim 𝐶)
96 oelim2 7840 . . . . . . . . . . . . . . 15 ((ω ∈ On ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → (ω ↑𝑜 𝐶) = 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑥))
9793, 94, 95, 96syl12anc 1475 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑𝑜 𝐶) = 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑥))
9892, 97eleqtrd 2837 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐴 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑥))
99 eliun 4672 . . . . . . . . . . . . 13 (𝐴 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑥) ↔ ∃𝑥 ∈ (𝐶 ∖ 1𝑜)𝐴 ∈ (ω ↑𝑜 𝑥))
10098, 99sylib 208 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → ∃𝑥 ∈ (𝐶 ∖ 1𝑜)𝐴 ∈ (ω ↑𝑜 𝑥))
101 eldifi 3871 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐶 ∖ 1𝑜) → 𝑥𝐶)
10218ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → 𝐴 ∈ On)
1039ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (ω ↑𝑜 𝐶) ∈ On)
10493adantr 472 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → ω ∈ On)
105 1onn 7884 . . . . . . . . . . . . . . . . . . . 20 1𝑜 ∈ ω
106105a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → 1𝑜 ∈ ω)
107 ondif2 7747 . . . . . . . . . . . . . . . . . . 19 (ω ∈ (On ∖ 2𝑜) ↔ (ω ∈ On ∧ 1𝑜 ∈ ω))
108104, 106, 107sylanbrc 701 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → ω ∈ (On ∖ 2𝑜))
10994adantr 472 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → 𝐶 ∈ On)
110 simplr 809 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → Lim 𝐶)
111 oelimcl 7845 . . . . . . . . . . . . . . . . . 18 ((ω ∈ (On ∖ 2𝑜) ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → Lim (ω ↑𝑜 𝐶))
112108, 109, 110, 111syl12anc 1475 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → Lim (ω ↑𝑜 𝐶))
113 oalim 7777 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ ((ω ↑𝑜 𝐶) ∈ On ∧ Lim (ω ↑𝑜 𝐶))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = 𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦))
114102, 103, 112, 113syl12anc 1475 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = 𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦))
115 oelim2 7840 . . . . . . . . . . . . . . . . . . . . . . 23 ((ω ∈ On ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → (ω ↑𝑜 𝐶) = 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑧))
11693, 94, 95, 115syl12anc 1475 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑𝑜 𝐶) = 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑧))
117116eleq2d 2821 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝑦 ∈ (ω ↑𝑜 𝐶) ↔ 𝑦 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑧)))
118 eliun 4672 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑧) ↔ ∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω ↑𝑜 𝑧))
119117, 118syl6bb 276 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝑦 ∈ (ω ↑𝑜 𝐶) ↔ ∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω ↑𝑜 𝑧)))
120119adantr 472 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (𝑦 ∈ (ω ↑𝑜 𝐶) ↔ ∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω ↑𝑜 𝑧)))
121 eldifi 3871 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ (𝐶 ∖ 1𝑜) → 𝑧𝐶)
122104adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ω ∈ On)
123109adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐶 ∈ On)
124 simplrl 819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑥𝐶)
125 onelon 5905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐶 ∈ On ∧ 𝑥𝐶) → 𝑥 ∈ On)
126123, 124, 125syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑥 ∈ On)
127122, 126, 46syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 𝑥) ∈ On)
128 eloni 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ω ↑𝑜 𝑥) ∈ On → Ord (ω ↑𝑜 𝑥))
129127, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → Ord (ω ↑𝑜 𝑥))
130 simplrr 820 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐴 ∈ (ω ↑𝑜 𝑥))
131 ordelss 5896 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Ord (ω ↑𝑜 𝑥) ∧ 𝐴 ∈ (ω ↑𝑜 𝑥)) → 𝐴 ⊆ (ω ↑𝑜 𝑥))
132129, 130, 131syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐴 ⊆ (ω ↑𝑜 𝑥))
133 ssun1 3915 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑥 ⊆ (𝑥𝑧)
13426ad3antrrr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → Ord 𝐶)
135 simprl 811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑧𝐶)
136 ordunel 7188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((Ord 𝐶𝑥𝐶𝑧𝐶) → (𝑥𝑧) ∈ 𝐶)
137134, 124, 135, 136syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑥𝑧) ∈ 𝐶)
138 onelon 5905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐶 ∈ On ∧ (𝑥𝑧) ∈ 𝐶) → (𝑥𝑧) ∈ On)
139123, 137, 138syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑥𝑧) ∈ On)
140 peano1 7246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ ∈ ω
141140a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ∅ ∈ ω)
142 oewordi 7836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 ∈ On ∧ (𝑥𝑧) ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (𝑥 ⊆ (𝑥𝑧) → (ω ↑𝑜 𝑥) ⊆ (ω ↑𝑜 (𝑥𝑧))))
143126, 139, 122, 141, 142syl31anc 1480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑥 ⊆ (𝑥𝑧) → (ω ↑𝑜 𝑥) ⊆ (ω ↑𝑜 (𝑥𝑧))))
144133, 143mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 𝑥) ⊆ (ω ↑𝑜 (𝑥𝑧)))
145132, 144sstrd 3750 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐴 ⊆ (ω ↑𝑜 (𝑥𝑧)))
146102adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐴 ∈ On)
147 oecl 7782 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ω ∈ On ∧ (𝑥𝑧) ∈ On) → (ω ↑𝑜 (𝑥𝑧)) ∈ On)
148122, 139, 147syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 (𝑥𝑧)) ∈ On)
149 onelon 5905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐶 ∈ On ∧ 𝑧𝐶) → 𝑧 ∈ On)
150123, 135, 149syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑧 ∈ On)
151 oecl 7782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ω ∈ On ∧ 𝑧 ∈ On) → (ω ↑𝑜 𝑧) ∈ On)
152122, 150, 151syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 𝑧) ∈ On)
153 simprr 813 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑦 ∈ (ω ↑𝑜 𝑧))
154 onelon 5905 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ω ↑𝑜 𝑧) ∈ On ∧ 𝑦 ∈ (ω ↑𝑜 𝑧)) → 𝑦 ∈ On)
155152, 153, 154syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑦 ∈ On)
156 oawordri 7795 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ On ∧ (ω ↑𝑜 (𝑥𝑧)) ∈ On ∧ 𝑦 ∈ On) → (𝐴 ⊆ (ω ↑𝑜 (𝑥𝑧)) → (𝐴 +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦)))
157146, 148, 155, 156syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 ⊆ (ω ↑𝑜 (𝑥𝑧)) → (𝐴 +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦)))
158145, 157mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦))
159 eloni 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ω ↑𝑜 𝑧) ∈ On → Ord (ω ↑𝑜 𝑧))
160152, 159syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → Ord (ω ↑𝑜 𝑧))
161 ordelss 5896 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Ord (ω ↑𝑜 𝑧) ∧ 𝑦 ∈ (ω ↑𝑜 𝑧)) → 𝑦 ⊆ (ω ↑𝑜 𝑧))
162160, 153, 161syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑦 ⊆ (ω ↑𝑜 𝑧))
163 ssun2 3916 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑧 ⊆ (𝑥𝑧)
164 oewordi 7836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑧 ∈ On ∧ (𝑥𝑧) ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (𝑧 ⊆ (𝑥𝑧) → (ω ↑𝑜 𝑧) ⊆ (ω ↑𝑜 (𝑥𝑧))))
165150, 139, 122, 141, 164syl31anc 1480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑧 ⊆ (𝑥𝑧) → (ω ↑𝑜 𝑧) ⊆ (ω ↑𝑜 (𝑥𝑧))))
166163, 165mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 𝑧) ⊆ (ω ↑𝑜 (𝑥𝑧)))
167162, 166sstrd 3750 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑦 ⊆ (ω ↑𝑜 (𝑥𝑧)))
168 oaword 7794 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ On ∧ (ω ↑𝑜 (𝑥𝑧)) ∈ On ∧ (ω ↑𝑜 (𝑥𝑧)) ∈ On) → (𝑦 ⊆ (ω ↑𝑜 (𝑥𝑧)) ↔ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧)))))
169155, 148, 148, 168syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑦 ⊆ (ω ↑𝑜 (𝑥𝑧)) ↔ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧)))))
170167, 169mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
171158, 170sstrd 3750 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
172 ordom 7235 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ord ω
173 ordsucss 7179 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Ord ω → (1𝑜 ∈ ω → suc 1𝑜 ⊆ ω))
174172, 105, 173mp2 9 . . . . . . . . . . . . . . . . . . . . . . . . . 26 suc 1𝑜 ⊆ ω
175 1on 7732 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1𝑜 ∈ On
176 suceloni 7174 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1𝑜 ∈ On → suc 1𝑜 ∈ On)
177175, 176mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → suc 1𝑜 ∈ On)
178 omwordi 7816 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((suc 1𝑜 ∈ On ∧ ω ∈ On ∧ (ω ↑𝑜 (𝑥𝑧)) ∈ On) → (suc 1𝑜 ⊆ ω → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) ⊆ ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω)))
179177, 122, 148, 178syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (suc 1𝑜 ⊆ ω → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) ⊆ ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω)))
180174, 179mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) ⊆ ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω))
181175a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 1𝑜 ∈ On)
182 omsuc 7771 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((ω ↑𝑜 (𝑥𝑧)) ∈ On ∧ 1𝑜 ∈ On) → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) = (((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
183148, 181, 182syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) = (((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
184 om1 7787 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ω ↑𝑜 (𝑥𝑧)) ∈ On → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) = (ω ↑𝑜 (𝑥𝑧)))
185148, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) = (ω ↑𝑜 (𝑥𝑧)))
186185oveq1d 6824 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) +𝑜 (ω ↑𝑜 (𝑥𝑧))) = ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
187183, 186eqtr2d 2791 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))) = ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜))
188 oesuc 7772 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ω ∈ On ∧ (𝑥𝑧) ∈ On) → (ω ↑𝑜 suc (𝑥𝑧)) = ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω))
189122, 139, 188syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 suc (𝑥𝑧)) = ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω))
190180, 187, 1893sstr4d 3785 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))) ⊆ (ω ↑𝑜 suc (𝑥𝑧)))
191171, 190sstrd 3750 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 suc (𝑥𝑧)))
192 ordsucss 7179 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord 𝐶 → ((𝑥𝑧) ∈ 𝐶 → suc (𝑥𝑧) ⊆ 𝐶))
193134, 137, 192sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → suc (𝑥𝑧) ⊆ 𝐶)
194 suceloni 7174 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥𝑧) ∈ On → suc (𝑥𝑧) ∈ On)
195139, 194syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → suc (𝑥𝑧) ∈ On)
196 oewordi 7836 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((suc (𝑥𝑧) ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (suc (𝑥𝑧) ⊆ 𝐶 → (ω ↑𝑜 suc (𝑥𝑧)) ⊆ (ω ↑𝑜 𝐶)))
197195, 123, 122, 141, 196syl31anc 1480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (suc (𝑥𝑧) ⊆ 𝐶 → (ω ↑𝑜 suc (𝑥𝑧)) ⊆ (ω ↑𝑜 𝐶)))
198193, 197mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 suc (𝑥𝑧)) ⊆ (ω ↑𝑜 𝐶))
199191, 198sstrd 3750 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶))
200199expr 644 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ 𝑧𝐶) → (𝑦 ∈ (ω ↑𝑜 𝑧) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶)))
201121, 200sylan2 492 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ 𝑧 ∈ (𝐶 ∖ 1𝑜)) → (𝑦 ∈ (ω ↑𝑜 𝑧) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶)))
202201rexlimdva 3165 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω ↑𝑜 𝑧) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶)))
203120, 202sylbid 230 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (𝑦 ∈ (ω ↑𝑜 𝐶) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶)))
204203ralrimiv 3099 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → ∀𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶))
205 iunss 4709 . . . . . . . . . . . . . . . . 17 ( 𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶) ↔ ∀𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶))
206204, 205sylibr 224 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → 𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶))
207114, 206eqsstrd 3776 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶))
208207expr 644 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ 𝑥𝐶) → (𝐴 ∈ (ω ↑𝑜 𝑥) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶)))
209101, 208sylan2 492 . . . . . . . . . . . . 13 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ 𝑥 ∈ (𝐶 ∖ 1𝑜)) → (𝐴 ∈ (ω ↑𝑜 𝑥) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶)))
210209rexlimdva 3165 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (∃𝑥 ∈ (𝐶 ∖ 1𝑜)𝐴 ∈ (ω ↑𝑜 𝑥) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶)))
211100, 210mpd 15 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶))
21288adantr 472 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑𝑜 𝐶) ⊆ (𝐴 +𝑜 (ω ↑𝑜 𝐶)))
213211, 212eqssd 3757 . . . . . . . . . 10 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
214213ex 449 . . . . . . . . 9 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (Lim 𝐶 → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶)))
21543, 91, 2143jaod 1537 . . . . . . . 8 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ((𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶)))
21628, 215mpd 15 . . . . . . 7 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
217216adantr 472 . . . . . 6 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
218217oveq1d 6824 . . . . 5 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +𝑜 (ω ↑𝑜 𝐶)) +𝑜 𝑥) = ((ω ↑𝑜 𝐶) +𝑜 𝑥))
21923, 218eqtr3d 2792 . . . 4 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)) = ((ω ↑𝑜 𝐶) +𝑜 𝑥))
220 oveq2 6817 . . . . 5 (((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → (𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)) = (𝐴 +𝑜 𝐵))
221 id 22 . . . . 5 (((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
222220, 221eqeq12d 2771 . . . 4 (((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → ((𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)) = ((ω ↑𝑜 𝐶) +𝑜 𝑥) ↔ (𝐴 +𝑜 𝐵) = 𝐵))
223219, 222syl5ibcom 235 . . 3 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → (𝐴 +𝑜 𝐵) = 𝐵))
224223rexlimdva 3165 . 2 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (∃𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → (𝐴 +𝑜 𝐵) = 𝐵))
22515, 224mpd 15 1 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐴 +𝑜 𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3o 1071   = wceq 1628  wcel 2135  wral 3046  wrex 3047  ∃!wreu 3048  cdif 3708  cun 3709  wss 3711  c0 4054   ciun 4668   × cxp 5260  dom cdm 5262  Ord word 5879  Oncon0 5880  Lim wlim 5881  suc csuc 5882   Fn wfn 6040  (class class class)co 6809  ωcom 7226  1𝑜c1o 7718  2𝑜c2o 7719   +𝑜 coa 7722   ·𝑜 comu 7723  𝑜 coe 7724
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-rep 4919  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-int 4624  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-1st 7329  df-2nd 7330  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-1o 7725  df-2o 7726  df-oadd 7729  df-omul 7730  df-oexp 7731
This theorem is referenced by:  cnfcomlem  8765
  Copyright terms: Public domain W3C validator