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

Theorem oaabs2 7612
Description: The absorption law oaabs 7611 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 3879 . . . . . . 7 (𝐴 ∈ (ω ↑𝑜 𝐶) → ¬ (ω ↑𝑜 𝐶) = ∅)
2 fnoe 7477 . . . . . . . . 9 𝑜 Fn (On × On)
3 fndm 5904 . . . . . . . . 9 ( ↑𝑜 Fn (On × On) → dom ↑𝑜 = (On × On))
42, 3ax-mp 5 . . . . . . . 8 dom ↑𝑜 = (On × On)
54ndmov 6716 . . . . . . 7 (¬ (ω ∈ On ∧ 𝐶 ∈ On) → (ω ↑𝑜 𝐶) = ∅)
61, 5nsyl2 141 . . . . . 6 (𝐴 ∈ (ω ↑𝑜 𝐶) → (ω ∈ On ∧ 𝐶 ∈ On))
76ad2antrr 758 . . . . 5 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ∈ On ∧ 𝐶 ∈ On))
8 oecl 7504 . . . . 5 ((ω ∈ On ∧ 𝐶 ∈ On) → (ω ↑𝑜 𝐶) ∈ On)
97, 8syl 17 . . . 4 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜 𝐶) ∈ On)
10 simplr 788 . . . 4 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → 𝐵 ∈ On)
11 simpr 476 . . . 4 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜 𝐶) ⊆ 𝐵)
12 oawordeu 7522 . . . 4 ((((ω ↑𝑜 𝐶) ∈ On ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ∃!𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
139, 10, 11, 12syl21anc 1317 . . 3 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ∃!𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
14 reurex 3137 . . 3 (∃!𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → ∃𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
1513, 14syl 17 . 2 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ∃𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
16 simpll 786 . . . . . . . 8 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → 𝐴 ∈ (ω ↑𝑜 𝐶))
17 onelon 5665 . . . . . . . 8 (((ω ↑𝑜 𝐶) ∈ On ∧ 𝐴 ∈ (ω ↑𝑜 𝐶)) → 𝐴 ∈ On)
189, 16, 17syl2anc 691 . . . . . . 7 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → 𝐴 ∈ On)
1918adantr 480 . . . . . 6 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝐴 ∈ On)
209adantr 480 . . . . . 6 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (ω ↑𝑜 𝐶) ∈ On)
21 simpr 476 . . . . . 6 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝑥 ∈ On)
22 oaass 7528 . . . . . 6 ((𝐴 ∈ On ∧ (ω ↑𝑜 𝐶) ∈ On ∧ 𝑥 ∈ On) → ((𝐴 +𝑜 (ω ↑𝑜 𝐶)) +𝑜 𝑥) = (𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)))
2319, 20, 21, 22syl3anc 1318 . . . . 5 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +𝑜 (ω ↑𝑜 𝐶)) +𝑜 𝑥) = (𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)))
247simprd 478 . . . . . . . . . 10 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → 𝐶 ∈ On)
25 eloni 5650 . . . . . . . . . 10 (𝐶 ∈ On → Ord 𝐶)
2624, 25syl 17 . . . . . . . . 9 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → Ord 𝐶)
27 ordzsl 6937 . . . . . . . . 9 (Ord 𝐶 ↔ (𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶))
2826, 27sylib 207 . . . . . . . 8 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶))
29 simplll 794 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 ∈ (ω ↑𝑜 𝐶))
30 oveq2 6557 . . . . . . . . . . . . . . 15 (𝐶 = ∅ → (ω ↑𝑜 𝐶) = (ω ↑𝑜 ∅))
317simpld 474 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ω ∈ On)
32 oe0 7489 . . . . . . . . . . . . . . . 16 (ω ∈ On → (ω ↑𝑜 ∅) = 1𝑜)
3331, 32syl 17 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜 ∅) = 1𝑜)
3430, 33sylan9eqr 2666 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (ω ↑𝑜 𝐶) = 1𝑜)
3529, 34eleqtrd 2690 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 ∈ 1𝑜)
36 el1o 7466 . . . . . . . . . . . . 13 (𝐴 ∈ 1𝑜𝐴 = ∅)
3735, 36sylib 207 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 = ∅)
3837oveq1d 6564 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (∅ +𝑜 (ω ↑𝑜 𝐶)))
399adantr 480 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (ω ↑𝑜 𝐶) ∈ On)
40 oa0r 7505 . . . . . . . . . . . 12 ((ω ↑𝑜 𝐶) ∈ On → (∅ +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
4139, 40syl 17 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (∅ +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
4238, 41eqtrd 2644 . . . . . . . . . 10 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
4342ex 449 . . . . . . . . 9 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐶 = ∅ → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶)))
4431adantr 480 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → ω ∈ On)
45 simprl 790 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝑥 ∈ On)
46 oecl 7504 . . . . . . . . . . . . . 14 ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑𝑜 𝑥) ∈ On)
4744, 45, 46syl2anc 691 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 𝑥) ∈ On)
48 limom 6972 . . . . . . . . . . . . . 14 Lim ω
4944, 48jctir 559 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ∈ On ∧ Lim ω))
50 simplll 794 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐴 ∈ (ω ↑𝑜 𝐶))
51 simprr 792 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐶 = suc 𝑥)
5251oveq2d 6565 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 𝐶) = (ω ↑𝑜 suc 𝑥))
53 oesuc 7494 . . . . . . . . . . . . . . . 16 ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑𝑜 suc 𝑥) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
5444, 45, 53syl2anc 691 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 suc 𝑥) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
5552, 54eqtrd 2644 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 𝐶) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
5650, 55eleqtrd 2690 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 ω))
57 omordlim 7544 . . . . . . . . . . . . 13 ((((ω ↑𝑜 𝑥) ∈ On ∧ (ω ∈ On ∧ Lim ω)) ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 ω)) → ∃𝑦 ∈ ω 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
5847, 49, 56, 57syl21anc 1317 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → ∃𝑦 ∈ ω 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
5947adantr 480 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (ω ↑𝑜 𝑥) ∈ On)
60 nnon 6963 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ω → 𝑦 ∈ On)
6160ad2antrl 760 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝑦 ∈ On)
62 omcl 7503 . . . . . . . . . . . . . . . . 17 (((ω ↑𝑜 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∈ On)
6359, 61, 62syl2anc 691 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → ((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∈ On)
64 eloni 5650 . . . . . . . . . . . . . . . 16 (((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∈ On → Ord ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
6563, 64syl 17 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → Ord ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
66 simprr 792 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
67 ordelss 5656 . . . . . . . . . . . . . . 15 ((Ord ((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦)) → 𝐴 ⊆ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
6865, 66, 67syl2anc 691 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝐴 ⊆ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
6918ad2antrr 758 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝐴 ∈ On)
709ad2antrr 758 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (ω ↑𝑜 𝐶) ∈ On)
71 oawordri 7517 . . . . . . . . . . . . . . 15 ((𝐴 ∈ On ∧ ((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∈ On ∧ (ω ↑𝑜 𝐶) ∈ On) → (𝐴 ⊆ ((ω ↑𝑜 𝑥) ·𝑜 𝑦) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶))))
7269, 63, 70, 71syl3anc 1318 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (𝐴 ⊆ ((ω ↑𝑜 𝑥) ·𝑜 𝑦) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶))))
7368, 72mpd 15 . . . . . . . . . . . . 13 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶)))
7444adantr 480 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → ω ∈ On)
75 odi 7546 . . . . . . . . . . . . . . . 16 (((ω ↑𝑜 𝑥) ∈ On ∧ 𝑦 ∈ On ∧ ω ∈ On) → ((ω ↑𝑜 𝑥) ·𝑜 (𝑦 +𝑜 ω)) = (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 ((ω ↑𝑜 𝑥) ·𝑜 ω)))
7659, 61, 74, 75syl3anc 1318 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → ((ω ↑𝑜 𝑥) ·𝑜 (𝑦 +𝑜 ω)) = (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 ((ω ↑𝑜 𝑥) ·𝑜 ω)))
77 simprl 790 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝑦 ∈ ω)
78 oaabslem 7610 . . . . . . . . . . . . . . . . 17 ((ω ∈ On ∧ 𝑦 ∈ ω) → (𝑦 +𝑜 ω) = ω)
7974, 77, 78syl2anc 691 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (𝑦 +𝑜 ω) = ω)
8079oveq2d 6565 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → ((ω ↑𝑜 𝑥) ·𝑜 (𝑦 +𝑜 ω)) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
8176, 80eqtr3d 2646 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 ((ω ↑𝑜 𝑥) ·𝑜 ω)) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
8255adantr 480 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (ω ↑𝑜 𝐶) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
8382oveq2d 6565 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶)) = (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 ((ω ↑𝑜 𝑥) ·𝑜 ω)))
8481, 83, 823eqtr4d 2654 . . . . . . . . . . . . 13 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
8573, 84sseqtrd 3604 . . . . . . . . . . . 12 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶))
8658, 85rexlimddv 3017 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶))
87 oaword2 7520 . . . . . . . . . . . . 13 (((ω ↑𝑜 𝐶) ∈ On ∧ 𝐴 ∈ On) → (ω ↑𝑜 𝐶) ⊆ (𝐴 +𝑜 (ω ↑𝑜 𝐶)))
889, 18, 87syl2anc 691 . . . . . . . . . . . 12 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜 𝐶) ⊆ (𝐴 +𝑜 (ω ↑𝑜 𝐶)))
8988adantr 480 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 𝐶) ⊆ (𝐴 +𝑜 (ω ↑𝑜 𝐶)))
9086, 89eqssd 3585 . . . . . . . . . 10 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
9190rexlimdvaa 3014 . . . . . . . . 9 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (∃𝑥 ∈ On 𝐶 = suc 𝑥 → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶)))
92 simplll 794 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐴 ∈ (ω ↑𝑜 𝐶))
9331adantr 480 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → ω ∈ On)
9424adantr 480 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐶 ∈ On)
95 simpr 476 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → Lim 𝐶)
96 oelim2 7562 . . . . . . . . . . . . . . 15 ((ω ∈ On ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → (ω ↑𝑜 𝐶) = 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑥))
9793, 94, 95, 96syl12anc 1316 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑𝑜 𝐶) = 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑥))
9892, 97eleqtrd 2690 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐴 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑥))
99 eliun 4460 . . . . . . . . . . . . 13 (𝐴 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑥) ↔ ∃𝑥 ∈ (𝐶 ∖ 1𝑜)𝐴 ∈ (ω ↑𝑜 𝑥))
10098, 99sylib 207 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → ∃𝑥 ∈ (𝐶 ∖ 1𝑜)𝐴 ∈ (ω ↑𝑜 𝑥))
101 eldifi 3694 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐶 ∖ 1𝑜) → 𝑥𝐶)
10218ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → 𝐴 ∈ On)
1039ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (ω ↑𝑜 𝐶) ∈ On)
10493adantr 480 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → ω ∈ On)
105 1onn 7606 . . . . . . . . . . . . . . . . . . . 20 1𝑜 ∈ ω
106105a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → 1𝑜 ∈ ω)
107 ondif2 7469 . . . . . . . . . . . . . . . . . . 19 (ω ∈ (On ∖ 2𝑜) ↔ (ω ∈ On ∧ 1𝑜 ∈ ω))
108104, 106, 107sylanbrc 695 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → ω ∈ (On ∖ 2𝑜))
10994adantr 480 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → 𝐶 ∈ On)
110 simplr 788 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → Lim 𝐶)
111 oelimcl 7567 . . . . . . . . . . . . . . . . . 18 ((ω ∈ (On ∖ 2𝑜) ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → Lim (ω ↑𝑜 𝐶))
112108, 109, 110, 111syl12anc 1316 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → Lim (ω ↑𝑜 𝐶))
113 oalim 7499 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ ((ω ↑𝑜 𝐶) ∈ On ∧ Lim (ω ↑𝑜 𝐶))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = 𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦))
114102, 103, 112, 113syl12anc 1316 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = 𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦))
115 oelim2 7562 . . . . . . . . . . . . . . . . . . . . . . 23 ((ω ∈ On ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → (ω ↑𝑜 𝐶) = 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑧))
11693, 94, 95, 115syl12anc 1316 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑𝑜 𝐶) = 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑧))
117116eleq2d 2673 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝑦 ∈ (ω ↑𝑜 𝐶) ↔ 𝑦 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑧)))
118 eliun 4460 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑧) ↔ ∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω ↑𝑜 𝑧))
119117, 118syl6bb 275 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝑦 ∈ (ω ↑𝑜 𝐶) ↔ ∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω ↑𝑜 𝑧)))
120119adantr 480 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (𝑦 ∈ (ω ↑𝑜 𝐶) ↔ ∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω ↑𝑜 𝑧)))
121 eldifi 3694 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ (𝐶 ∖ 1𝑜) → 𝑧𝐶)
122104adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ω ∈ On)
123109adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐶 ∈ On)
124 simplrl 796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑥𝐶)
125 onelon 5665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐶 ∈ On ∧ 𝑥𝐶) → 𝑥 ∈ On)
126123, 124, 125syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑥 ∈ On)
127122, 126, 46syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 𝑥) ∈ On)
128 eloni 5650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ω ↑𝑜 𝑥) ∈ On → Ord (ω ↑𝑜 𝑥))
129127, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → Ord (ω ↑𝑜 𝑥))
130 simplrr 797 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐴 ∈ (ω ↑𝑜 𝑥))
131 ordelss 5656 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Ord (ω ↑𝑜 𝑥) ∧ 𝐴 ∈ (ω ↑𝑜 𝑥)) → 𝐴 ⊆ (ω ↑𝑜 𝑥))
132129, 130, 131syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐴 ⊆ (ω ↑𝑜 𝑥))
133 ssun1 3738 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑥 ⊆ (𝑥𝑧)
13426ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → Ord 𝐶)
135 simprl 790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑧𝐶)
136 ordunel 6919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((Ord 𝐶𝑥𝐶𝑧𝐶) → (𝑥𝑧) ∈ 𝐶)
137134, 124, 135, 136syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑥𝑧) ∈ 𝐶)
138 onelon 5665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐶 ∈ On ∧ (𝑥𝑧) ∈ 𝐶) → (𝑥𝑧) ∈ On)
139123, 137, 138syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑥𝑧) ∈ On)
140 peano1 6977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ ∈ ω
141140a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ∅ ∈ ω)
142 oewordi 7558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 ∈ On ∧ (𝑥𝑧) ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (𝑥 ⊆ (𝑥𝑧) → (ω ↑𝑜 𝑥) ⊆ (ω ↑𝑜 (𝑥𝑧))))
143126, 139, 122, 141, 142syl31anc 1321 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑥 ⊆ (𝑥𝑧) → (ω ↑𝑜 𝑥) ⊆ (ω ↑𝑜 (𝑥𝑧))))
144133, 143mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 𝑥) ⊆ (ω ↑𝑜 (𝑥𝑧)))
145132, 144sstrd 3578 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐴 ⊆ (ω ↑𝑜 (𝑥𝑧)))
146102adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐴 ∈ On)
147 oecl 7504 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ω ∈ On ∧ (𝑥𝑧) ∈ On) → (ω ↑𝑜 (𝑥𝑧)) ∈ On)
148122, 139, 147syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 (𝑥𝑧)) ∈ On)
149 onelon 5665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐶 ∈ On ∧ 𝑧𝐶) → 𝑧 ∈ On)
150123, 135, 149syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑧 ∈ On)
151 oecl 7504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ω ∈ On ∧ 𝑧 ∈ On) → (ω ↑𝑜 𝑧) ∈ On)
152122, 150, 151syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 𝑧) ∈ On)
153 simprr 792 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑦 ∈ (ω ↑𝑜 𝑧))
154 onelon 5665 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ω ↑𝑜 𝑧) ∈ On ∧ 𝑦 ∈ (ω ↑𝑜 𝑧)) → 𝑦 ∈ On)
155152, 153, 154syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑦 ∈ On)
156 oawordri 7517 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ On ∧ (ω ↑𝑜 (𝑥𝑧)) ∈ On ∧ 𝑦 ∈ On) → (𝐴 ⊆ (ω ↑𝑜 (𝑥𝑧)) → (𝐴 +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦)))
157146, 148, 155, 156syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 ⊆ (ω ↑𝑜 (𝑥𝑧)) → (𝐴 +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦)))
158145, 157mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦))
159 eloni 5650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ω ↑𝑜 𝑧) ∈ On → Ord (ω ↑𝑜 𝑧))
160152, 159syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → Ord (ω ↑𝑜 𝑧))
161 ordelss 5656 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Ord (ω ↑𝑜 𝑧) ∧ 𝑦 ∈ (ω ↑𝑜 𝑧)) → 𝑦 ⊆ (ω ↑𝑜 𝑧))
162160, 153, 161syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑦 ⊆ (ω ↑𝑜 𝑧))
163 ssun2 3739 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑧 ⊆ (𝑥𝑧)
164 oewordi 7558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑧 ∈ On ∧ (𝑥𝑧) ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (𝑧 ⊆ (𝑥𝑧) → (ω ↑𝑜 𝑧) ⊆ (ω ↑𝑜 (𝑥𝑧))))
165150, 139, 122, 141, 164syl31anc 1321 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑧 ⊆ (𝑥𝑧) → (ω ↑𝑜 𝑧) ⊆ (ω ↑𝑜 (𝑥𝑧))))
166163, 165mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 𝑧) ⊆ (ω ↑𝑜 (𝑥𝑧)))
167162, 166sstrd 3578 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑦 ⊆ (ω ↑𝑜 (𝑥𝑧)))
168 oaword 7516 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ On ∧ (ω ↑𝑜 (𝑥𝑧)) ∈ On ∧ (ω ↑𝑜 (𝑥𝑧)) ∈ On) → (𝑦 ⊆ (ω ↑𝑜 (𝑥𝑧)) ↔ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧)))))
169155, 148, 148, 168syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑦 ⊆ (ω ↑𝑜 (𝑥𝑧)) ↔ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧)))))
170167, 169mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
171158, 170sstrd 3578 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
172 ordom 6966 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ord ω
173 ordsucss 6910 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Ord ω → (1𝑜 ∈ ω → suc 1𝑜 ⊆ ω))
174172, 105, 173mp2 9 . . . . . . . . . . . . . . . . . . . . . . . . . 26 suc 1𝑜 ⊆ ω
175 1on 7454 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1𝑜 ∈ On
176 suceloni 6905 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1𝑜 ∈ On → suc 1𝑜 ∈ On)
177175, 176mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → suc 1𝑜 ∈ On)
178 omwordi 7538 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((suc 1𝑜 ∈ On ∧ ω ∈ On ∧ (ω ↑𝑜 (𝑥𝑧)) ∈ On) → (suc 1𝑜 ⊆ ω → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) ⊆ ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω)))
179177, 122, 148, 178syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (suc 1𝑜 ⊆ ω → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) ⊆ ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω)))
180174, 179mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) ⊆ ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω))
181175a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 1𝑜 ∈ On)
182 omsuc 7493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((ω ↑𝑜 (𝑥𝑧)) ∈ On ∧ 1𝑜 ∈ On) → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) = (((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
183148, 181, 182syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) = (((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
184 om1 7509 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ω ↑𝑜 (𝑥𝑧)) ∈ On → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) = (ω ↑𝑜 (𝑥𝑧)))
185148, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) = (ω ↑𝑜 (𝑥𝑧)))
186185oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) +𝑜 (ω ↑𝑜 (𝑥𝑧))) = ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
187183, 186eqtr2d 2645 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))) = ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜))
188 oesuc 7494 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ω ∈ On ∧ (𝑥𝑧) ∈ On) → (ω ↑𝑜 suc (𝑥𝑧)) = ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω))
189122, 139, 188syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 suc (𝑥𝑧)) = ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω))
190180, 187, 1893sstr4d 3611 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))) ⊆ (ω ↑𝑜 suc (𝑥𝑧)))
191171, 190sstrd 3578 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 suc (𝑥𝑧)))
192 ordsucss 6910 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord 𝐶 → ((𝑥𝑧) ∈ 𝐶 → suc (𝑥𝑧) ⊆ 𝐶))
193134, 137, 192sylc 63 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → suc (𝑥𝑧) ⊆ 𝐶)
194 suceloni 6905 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥𝑧) ∈ On → suc (𝑥𝑧) ∈ On)
195139, 194syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → suc (𝑥𝑧) ∈ On)
196 oewordi 7558 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((suc (𝑥𝑧) ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (suc (𝑥𝑧) ⊆ 𝐶 → (ω ↑𝑜 suc (𝑥𝑧)) ⊆ (ω ↑𝑜 𝐶)))
197195, 123, 122, 141, 196syl31anc 1321 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (suc (𝑥𝑧) ⊆ 𝐶 → (ω ↑𝑜 suc (𝑥𝑧)) ⊆ (ω ↑𝑜 𝐶)))
198193, 197mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 suc (𝑥𝑧)) ⊆ (ω ↑𝑜 𝐶))
199191, 198sstrd 3578 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶))
200199expr 641 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ 𝑧𝐶) → (𝑦 ∈ (ω ↑𝑜 𝑧) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶)))
201121, 200sylan2 490 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ 𝑧 ∈ (𝐶 ∖ 1𝑜)) → (𝑦 ∈ (ω ↑𝑜 𝑧) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶)))
202201rexlimdva 3013 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω ↑𝑜 𝑧) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶)))
203120, 202sylbid 229 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (𝑦 ∈ (ω ↑𝑜 𝐶) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶)))
204203ralrimiv 2948 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → ∀𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶))
205 iunss 4497 . . . . . . . . . . . . . . . . 17 ( 𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶) ↔ ∀𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶))
206204, 205sylibr 223 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → 𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶))
207114, 206eqsstrd 3602 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶))
208207expr 641 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ 𝑥𝐶) → (𝐴 ∈ (ω ↑𝑜 𝑥) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶)))
209101, 208sylan2 490 . . . . . . . . . . . . 13 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ 𝑥 ∈ (𝐶 ∖ 1𝑜)) → (𝐴 ∈ (ω ↑𝑜 𝑥) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶)))
210209rexlimdva 3013 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (∃𝑥 ∈ (𝐶 ∖ 1𝑜)𝐴 ∈ (ω ↑𝑜 𝑥) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶)))
211100, 210mpd 15 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶))
21288adantr 480 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑𝑜 𝐶) ⊆ (𝐴 +𝑜 (ω ↑𝑜 𝐶)))
213211, 212eqssd 3585 . . . . . . . . . 10 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
214213ex 449 . . . . . . . . 9 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (Lim 𝐶 → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶)))
21543, 91, 2143jaod 1384 . . . . . . . 8 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ((𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶)))
21628, 215mpd 15 . . . . . . 7 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
217216adantr 480 . . . . . 6 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
218217oveq1d 6564 . . . . 5 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +𝑜 (ω ↑𝑜 𝐶)) +𝑜 𝑥) = ((ω ↑𝑜 𝐶) +𝑜 𝑥))
21923, 218eqtr3d 2646 . . . 4 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)) = ((ω ↑𝑜 𝐶) +𝑜 𝑥))
220 oveq2 6557 . . . . 5 (((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → (𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)) = (𝐴 +𝑜 𝐵))
221 id 22 . . . . 5 (((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
222220, 221eqeq12d 2625 . . . 4 (((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → ((𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)) = ((ω ↑𝑜 𝐶) +𝑜 𝑥) ↔ (𝐴 +𝑜 𝐵) = 𝐵))
223219, 222syl5ibcom 234 . . 3 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → (𝐴 +𝑜 𝐵) = 𝐵))
224223rexlimdva 3013 . 2 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (∃𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → (𝐴 +𝑜 𝐵) = 𝐵))
22515, 224mpd 15 1 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐴 +𝑜 𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  w3o 1030   = wceq 1475  wcel 1977  wral 2896  wrex 2897  ∃!wreu 2898  cdif 3537  cun 3538  wss 3540  c0 3874   ciun 4455   × cxp 5036  dom cdm 5038  Ord word 5639  Oncon0 5640  Lim wlim 5641  suc csuc 5642   Fn wfn 5799  (class class class)co 6549  ωcom 6957  1𝑜c1o 7440  2𝑜c2o 7441   +𝑜 coa 7444   ·𝑜 comu 7445  𝑜 coe 7446
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-omul 7452  df-oexp 7453
This theorem is referenced by:  cnfcomlem  8479
  Copyright terms: Public domain W3C validator