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

Theorem oaabs2 7670
Description: The absorption law oaabs 7669 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 3896 . . . . . . 7 (𝐴 ∈ (ω ↑𝑜 𝐶) → ¬ (ω ↑𝑜 𝐶) = ∅)
2 fnoe 7535 . . . . . . . . 9 𝑜 Fn (On × On)
3 fndm 5948 . . . . . . . . 9 ( ↑𝑜 Fn (On × On) → dom ↑𝑜 = (On × On))
42, 3ax-mp 5 . . . . . . . 8 dom ↑𝑜 = (On × On)
54ndmov 6771 . . . . . . 7 (¬ (ω ∈ On ∧ 𝐶 ∈ On) → (ω ↑𝑜 𝐶) = ∅)
61, 5nsyl2 142 . . . . . 6 (𝐴 ∈ (ω ↑𝑜 𝐶) → (ω ∈ On ∧ 𝐶 ∈ On))
76ad2antrr 761 . . . . 5 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ∈ On ∧ 𝐶 ∈ On))
8 oecl 7562 . . . . 5 ((ω ∈ On ∧ 𝐶 ∈ On) → (ω ↑𝑜 𝐶) ∈ On)
97, 8syl 17 . . . 4 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜 𝐶) ∈ On)
10 simplr 791 . . . 4 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → 𝐵 ∈ On)
11 simpr 477 . . . 4 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜 𝐶) ⊆ 𝐵)
12 oawordeu 7580 . . . 4 ((((ω ↑𝑜 𝐶) ∈ On ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ∃!𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
139, 10, 11, 12syl21anc 1322 . . 3 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ∃!𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
14 reurex 3149 . . 3 (∃!𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → ∃𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
1513, 14syl 17 . 2 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ∃𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
16 simpll 789 . . . . . . . 8 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → 𝐴 ∈ (ω ↑𝑜 𝐶))
17 onelon 5707 . . . . . . . 8 (((ω ↑𝑜 𝐶) ∈ On ∧ 𝐴 ∈ (ω ↑𝑜 𝐶)) → 𝐴 ∈ On)
189, 16, 17syl2anc 692 . . . . . . 7 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → 𝐴 ∈ On)
1918adantr 481 . . . . . 6 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝐴 ∈ On)
209adantr 481 . . . . . 6 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (ω ↑𝑜 𝐶) ∈ On)
21 simpr 477 . . . . . 6 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝑥 ∈ On)
22 oaass 7586 . . . . . 6 ((𝐴 ∈ On ∧ (ω ↑𝑜 𝐶) ∈ On ∧ 𝑥 ∈ On) → ((𝐴 +𝑜 (ω ↑𝑜 𝐶)) +𝑜 𝑥) = (𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)))
2319, 20, 21, 22syl3anc 1323 . . . . 5 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +𝑜 (ω ↑𝑜 𝐶)) +𝑜 𝑥) = (𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)))
247simprd 479 . . . . . . . . . 10 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → 𝐶 ∈ On)
25 eloni 5692 . . . . . . . . . 10 (𝐶 ∈ On → Ord 𝐶)
2624, 25syl 17 . . . . . . . . 9 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → Ord 𝐶)
27 ordzsl 6992 . . . . . . . . 9 (Ord 𝐶 ↔ (𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶))
2826, 27sylib 208 . . . . . . . 8 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶))
29 simplll 797 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 ∈ (ω ↑𝑜 𝐶))
30 oveq2 6612 . . . . . . . . . . . . . . 15 (𝐶 = ∅ → (ω ↑𝑜 𝐶) = (ω ↑𝑜 ∅))
317simpld 475 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ω ∈ On)
32 oe0 7547 . . . . . . . . . . . . . . . 16 (ω ∈ On → (ω ↑𝑜 ∅) = 1𝑜)
3331, 32syl 17 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜 ∅) = 1𝑜)
3430, 33sylan9eqr 2677 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (ω ↑𝑜 𝐶) = 1𝑜)
3529, 34eleqtrd 2700 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 ∈ 1𝑜)
36 el1o 7524 . . . . . . . . . . . . 13 (𝐴 ∈ 1𝑜𝐴 = ∅)
3735, 36sylib 208 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 = ∅)
3837oveq1d 6619 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (∅ +𝑜 (ω ↑𝑜 𝐶)))
399adantr 481 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (ω ↑𝑜 𝐶) ∈ On)
40 oa0r 7563 . . . . . . . . . . . 12 ((ω ↑𝑜 𝐶) ∈ On → (∅ +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
4139, 40syl 17 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (∅ +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
4238, 41eqtrd 2655 . . . . . . . . . 10 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
4342ex 450 . . . . . . . . 9 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐶 = ∅ → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶)))
4431adantr 481 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → ω ∈ On)
45 simprl 793 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝑥 ∈ On)
46 oecl 7562 . . . . . . . . . . . . . 14 ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑𝑜 𝑥) ∈ On)
4744, 45, 46syl2anc 692 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 𝑥) ∈ On)
48 limom 7027 . . . . . . . . . . . . . 14 Lim ω
4944, 48jctir 560 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ∈ On ∧ Lim ω))
50 simplll 797 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐴 ∈ (ω ↑𝑜 𝐶))
51 simprr 795 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐶 = suc 𝑥)
5251oveq2d 6620 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 𝐶) = (ω ↑𝑜 suc 𝑥))
53 oesuc 7552 . . . . . . . . . . . . . . . 16 ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑𝑜 suc 𝑥) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
5444, 45, 53syl2anc 692 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 suc 𝑥) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
5552, 54eqtrd 2655 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 𝐶) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
5650, 55eleqtrd 2700 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 ω))
57 omordlim 7602 . . . . . . . . . . . . 13 ((((ω ↑𝑜 𝑥) ∈ On ∧ (ω ∈ On ∧ Lim ω)) ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 ω)) → ∃𝑦 ∈ ω 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
5847, 49, 56, 57syl21anc 1322 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → ∃𝑦 ∈ ω 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
5947adantr 481 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (ω ↑𝑜 𝑥) ∈ On)
60 nnon 7018 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ω → 𝑦 ∈ On)
6160ad2antrl 763 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝑦 ∈ On)
62 omcl 7561 . . . . . . . . . . . . . . . . 17 (((ω ↑𝑜 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∈ On)
6359, 61, 62syl2anc 692 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → ((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∈ On)
64 eloni 5692 . . . . . . . . . . . . . . . 16 (((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∈ On → Ord ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
6563, 64syl 17 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → Ord ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
66 simprr 795 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
67 ordelss 5698 . . . . . . . . . . . . . . 15 ((Ord ((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦)) → 𝐴 ⊆ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
6865, 66, 67syl2anc 692 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝐴 ⊆ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))
6918ad2antrr 761 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝐴 ∈ On)
709ad2antrr 761 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (ω ↑𝑜 𝐶) ∈ On)
71 oawordri 7575 . . . . . . . . . . . . . . 15 ((𝐴 ∈ On ∧ ((ω ↑𝑜 𝑥) ·𝑜 𝑦) ∈ On ∧ (ω ↑𝑜 𝐶) ∈ On) → (𝐴 ⊆ ((ω ↑𝑜 𝑥) ·𝑜 𝑦) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶))))
7269, 63, 70, 71syl3anc 1323 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (𝐴 ⊆ ((ω ↑𝑜 𝑥) ·𝑜 𝑦) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶))))
7368, 72mpd 15 . . . . . . . . . . . . 13 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶)))
7444adantr 481 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → ω ∈ On)
75 odi 7604 . . . . . . . . . . . . . . . 16 (((ω ↑𝑜 𝑥) ∈ On ∧ 𝑦 ∈ On ∧ ω ∈ On) → ((ω ↑𝑜 𝑥) ·𝑜 (𝑦 +𝑜 ω)) = (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 ((ω ↑𝑜 𝑥) ·𝑜 ω)))
7659, 61, 74, 75syl3anc 1323 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → ((ω ↑𝑜 𝑥) ·𝑜 (𝑦 +𝑜 ω)) = (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 ((ω ↑𝑜 𝑥) ·𝑜 ω)))
77 simprl 793 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → 𝑦 ∈ ω)
78 oaabslem 7668 . . . . . . . . . . . . . . . . 17 ((ω ∈ On ∧ 𝑦 ∈ ω) → (𝑦 +𝑜 ω) = ω)
7974, 77, 78syl2anc 692 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (𝑦 +𝑜 ω) = ω)
8079oveq2d 6620 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → ((ω ↑𝑜 𝑥) ·𝑜 (𝑦 +𝑜 ω)) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
8176, 80eqtr3d 2657 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 ((ω ↑𝑜 𝑥) ·𝑜 ω)) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
8255adantr 481 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (ω ↑𝑜 𝐶) = ((ω ↑𝑜 𝑥) ·𝑜 ω))
8382oveq2d 6620 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶)) = (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 ((ω ↑𝑜 𝑥) ·𝑜 ω)))
8481, 83, 823eqtr4d 2665 . . . . . . . . . . . . 13 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (((ω ↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
8573, 84sseqtrd 3620 . . . . . . . . . . . 12 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑𝑜 𝑥) ·𝑜 𝑦))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶))
8658, 85rexlimddv 3028 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶))
87 oaword2 7578 . . . . . . . . . . . . 13 (((ω ↑𝑜 𝐶) ∈ On ∧ 𝐴 ∈ On) → (ω ↑𝑜 𝐶) ⊆ (𝐴 +𝑜 (ω ↑𝑜 𝐶)))
889, 18, 87syl2anc 692 . . . . . . . . . . . 12 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (ω ↑𝑜 𝐶) ⊆ (𝐴 +𝑜 (ω ↑𝑜 𝐶)))
8988adantr 481 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑𝑜 𝐶) ⊆ (𝐴 +𝑜 (ω ↑𝑜 𝐶)))
9086, 89eqssd 3600 . . . . . . . . . 10 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
9190rexlimdvaa 3025 . . . . . . . . 9 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (∃𝑥 ∈ On 𝐶 = suc 𝑥 → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶)))
92 simplll 797 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐴 ∈ (ω ↑𝑜 𝐶))
9331adantr 481 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → ω ∈ On)
9424adantr 481 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐶 ∈ On)
95 simpr 477 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → Lim 𝐶)
96 oelim2 7620 . . . . . . . . . . . . . . 15 ((ω ∈ On ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → (ω ↑𝑜 𝐶) = 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑥))
9793, 94, 95, 96syl12anc 1321 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑𝑜 𝐶) = 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑥))
9892, 97eleqtrd 2700 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐴 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑥))
99 eliun 4490 . . . . . . . . . . . . 13 (𝐴 𝑥 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑥) ↔ ∃𝑥 ∈ (𝐶 ∖ 1𝑜)𝐴 ∈ (ω ↑𝑜 𝑥))
10098, 99sylib 208 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → ∃𝑥 ∈ (𝐶 ∖ 1𝑜)𝐴 ∈ (ω ↑𝑜 𝑥))
101 eldifi 3710 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐶 ∖ 1𝑜) → 𝑥𝐶)
10218ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → 𝐴 ∈ On)
1039ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (ω ↑𝑜 𝐶) ∈ On)
10493adantr 481 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → ω ∈ On)
105 1onn 7664 . . . . . . . . . . . . . . . . . . . 20 1𝑜 ∈ ω
106105a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → 1𝑜 ∈ ω)
107 ondif2 7527 . . . . . . . . . . . . . . . . . . 19 (ω ∈ (On ∖ 2𝑜) ↔ (ω ∈ On ∧ 1𝑜 ∈ ω))
108104, 106, 107sylanbrc 697 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → ω ∈ (On ∖ 2𝑜))
10994adantr 481 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → 𝐶 ∈ On)
110 simplr 791 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → Lim 𝐶)
111 oelimcl 7625 . . . . . . . . . . . . . . . . . 18 ((ω ∈ (On ∖ 2𝑜) ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → Lim (ω ↑𝑜 𝐶))
112108, 109, 110, 111syl12anc 1321 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → Lim (ω ↑𝑜 𝐶))
113 oalim 7557 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ ((ω ↑𝑜 𝐶) ∈ On ∧ Lim (ω ↑𝑜 𝐶))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = 𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦))
114102, 103, 112, 113syl12anc 1321 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = 𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦))
115 oelim2 7620 . . . . . . . . . . . . . . . . . . . . . . 23 ((ω ∈ On ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → (ω ↑𝑜 𝐶) = 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑧))
11693, 94, 95, 115syl12anc 1321 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑𝑜 𝐶) = 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑧))
117116eleq2d 2684 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝑦 ∈ (ω ↑𝑜 𝐶) ↔ 𝑦 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑧)))
118 eliun 4490 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 𝑧 ∈ (𝐶 ∖ 1𝑜)(ω ↑𝑜 𝑧) ↔ ∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω ↑𝑜 𝑧))
119117, 118syl6bb 276 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝑦 ∈ (ω ↑𝑜 𝐶) ↔ ∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω ↑𝑜 𝑧)))
120119adantr 481 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (𝑦 ∈ (ω ↑𝑜 𝐶) ↔ ∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω ↑𝑜 𝑧)))
121 eldifi 3710 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ (𝐶 ∖ 1𝑜) → 𝑧𝐶)
122104adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ω ∈ On)
123109adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐶 ∈ On)
124 simplrl 799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑥𝐶)
125 onelon 5707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐶 ∈ On ∧ 𝑥𝐶) → 𝑥 ∈ On)
126123, 124, 125syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑥 ∈ On)
127122, 126, 46syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 𝑥) ∈ On)
128 eloni 5692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ω ↑𝑜 𝑥) ∈ On → Ord (ω ↑𝑜 𝑥))
129127, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → Ord (ω ↑𝑜 𝑥))
130 simplrr 800 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐴 ∈ (ω ↑𝑜 𝑥))
131 ordelss 5698 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Ord (ω ↑𝑜 𝑥) ∧ 𝐴 ∈ (ω ↑𝑜 𝑥)) → 𝐴 ⊆ (ω ↑𝑜 𝑥))
132129, 130, 131syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐴 ⊆ (ω ↑𝑜 𝑥))
133 ssun1 3754 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑥 ⊆ (𝑥𝑧)
13426ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → Ord 𝐶)
135 simprl 793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑧𝐶)
136 ordunel 6974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((Ord 𝐶𝑥𝐶𝑧𝐶) → (𝑥𝑧) ∈ 𝐶)
137134, 124, 135, 136syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑥𝑧) ∈ 𝐶)
138 onelon 5707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐶 ∈ On ∧ (𝑥𝑧) ∈ 𝐶) → (𝑥𝑧) ∈ On)
139123, 137, 138syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑥𝑧) ∈ On)
140 peano1 7032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ ∈ ω
141140a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ∅ ∈ ω)
142 oewordi 7616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 ∈ On ∧ (𝑥𝑧) ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (𝑥 ⊆ (𝑥𝑧) → (ω ↑𝑜 𝑥) ⊆ (ω ↑𝑜 (𝑥𝑧))))
143126, 139, 122, 141, 142syl31anc 1326 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑥 ⊆ (𝑥𝑧) → (ω ↑𝑜 𝑥) ⊆ (ω ↑𝑜 (𝑥𝑧))))
144133, 143mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 𝑥) ⊆ (ω ↑𝑜 (𝑥𝑧)))
145132, 144sstrd 3593 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐴 ⊆ (ω ↑𝑜 (𝑥𝑧)))
146102adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝐴 ∈ On)
147 oecl 7562 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ω ∈ On ∧ (𝑥𝑧) ∈ On) → (ω ↑𝑜 (𝑥𝑧)) ∈ On)
148122, 139, 147syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 (𝑥𝑧)) ∈ On)
149 onelon 5707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐶 ∈ On ∧ 𝑧𝐶) → 𝑧 ∈ On)
150123, 135, 149syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑧 ∈ On)
151 oecl 7562 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ω ∈ On ∧ 𝑧 ∈ On) → (ω ↑𝑜 𝑧) ∈ On)
152122, 150, 151syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 𝑧) ∈ On)
153 simprr 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑦 ∈ (ω ↑𝑜 𝑧))
154 onelon 5707 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ω ↑𝑜 𝑧) ∈ On ∧ 𝑦 ∈ (ω ↑𝑜 𝑧)) → 𝑦 ∈ On)
155152, 153, 154syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑦 ∈ On)
156 oawordri 7575 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ On ∧ (ω ↑𝑜 (𝑥𝑧)) ∈ On ∧ 𝑦 ∈ On) → (𝐴 ⊆ (ω ↑𝑜 (𝑥𝑧)) → (𝐴 +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦)))
157146, 148, 155, 156syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 ⊆ (ω ↑𝑜 (𝑥𝑧)) → (𝐴 +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦)))
158145, 157mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦))
159 eloni 5692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ω ↑𝑜 𝑧) ∈ On → Ord (ω ↑𝑜 𝑧))
160152, 159syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → Ord (ω ↑𝑜 𝑧))
161 ordelss 5698 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Ord (ω ↑𝑜 𝑧) ∧ 𝑦 ∈ (ω ↑𝑜 𝑧)) → 𝑦 ⊆ (ω ↑𝑜 𝑧))
162160, 153, 161syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑦 ⊆ (ω ↑𝑜 𝑧))
163 ssun2 3755 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑧 ⊆ (𝑥𝑧)
164 oewordi 7616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑧 ∈ On ∧ (𝑥𝑧) ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (𝑧 ⊆ (𝑥𝑧) → (ω ↑𝑜 𝑧) ⊆ (ω ↑𝑜 (𝑥𝑧))))
165150, 139, 122, 141, 164syl31anc 1326 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑧 ⊆ (𝑥𝑧) → (ω ↑𝑜 𝑧) ⊆ (ω ↑𝑜 (𝑥𝑧))))
166163, 165mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 𝑧) ⊆ (ω ↑𝑜 (𝑥𝑧)))
167162, 166sstrd 3593 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 𝑦 ⊆ (ω ↑𝑜 (𝑥𝑧)))
168 oaword 7574 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ On ∧ (ω ↑𝑜 (𝑥𝑧)) ∈ On ∧ (ω ↑𝑜 (𝑥𝑧)) ∈ On) → (𝑦 ⊆ (ω ↑𝑜 (𝑥𝑧)) ↔ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧)))))
169155, 148, 148, 168syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝑦 ⊆ (ω ↑𝑜 (𝑥𝑧)) ↔ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧)))))
170167, 169mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
171158, 170sstrd 3593 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 +𝑜 𝑦) ⊆ ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
172 ordom 7021 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ord ω
173 ordsucss 6965 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Ord ω → (1𝑜 ∈ ω → suc 1𝑜 ⊆ ω))
174172, 105, 173mp2 9 . . . . . . . . . . . . . . . . . . . . . . . . . 26 suc 1𝑜 ⊆ ω
175 1on 7512 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1𝑜 ∈ On
176 suceloni 6960 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1𝑜 ∈ On → suc 1𝑜 ∈ On)
177175, 176mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → suc 1𝑜 ∈ On)
178 omwordi 7596 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((suc 1𝑜 ∈ On ∧ ω ∈ On ∧ (ω ↑𝑜 (𝑥𝑧)) ∈ On) → (suc 1𝑜 ⊆ ω → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) ⊆ ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω)))
179177, 122, 148, 178syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (suc 1𝑜 ⊆ ω → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) ⊆ ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω)))
180174, 179mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) ⊆ ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω))
181175a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → 1𝑜 ∈ On)
182 omsuc 7551 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((ω ↑𝑜 (𝑥𝑧)) ∈ On ∧ 1𝑜 ∈ On) → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) = (((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
183148, 181, 182syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜) = (((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
184 om1 7567 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ω ↑𝑜 (𝑥𝑧)) ∈ On → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) = (ω ↑𝑜 (𝑥𝑧)))
185148, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) = (ω ↑𝑜 (𝑥𝑧)))
186185oveq1d 6619 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (((ω ↑𝑜 (𝑥𝑧)) ·𝑜 1𝑜) +𝑜 (ω ↑𝑜 (𝑥𝑧))) = ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))))
187183, 186eqtr2d 2656 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))) = ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 suc 1𝑜))
188 oesuc 7552 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ω ∈ On ∧ (𝑥𝑧) ∈ On) → (ω ↑𝑜 suc (𝑥𝑧)) = ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω))
189122, 139, 188syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 suc (𝑥𝑧)) = ((ω ↑𝑜 (𝑥𝑧)) ·𝑜 ω))
190180, 187, 1893sstr4d 3627 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → ((ω ↑𝑜 (𝑥𝑧)) +𝑜 (ω ↑𝑜 (𝑥𝑧))) ⊆ (ω ↑𝑜 suc (𝑥𝑧)))
191171, 190sstrd 3593 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 suc (𝑥𝑧)))
192 ordsucss 6965 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord 𝐶 → ((𝑥𝑧) ∈ 𝐶 → suc (𝑥𝑧) ⊆ 𝐶))
193134, 137, 192sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → suc (𝑥𝑧) ⊆ 𝐶)
194 suceloni 6960 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥𝑧) ∈ On → suc (𝑥𝑧) ∈ On)
195139, 194syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → suc (𝑥𝑧) ∈ On)
196 oewordi 7616 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((suc (𝑥𝑧) ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (suc (𝑥𝑧) ⊆ 𝐶 → (ω ↑𝑜 suc (𝑥𝑧)) ⊆ (ω ↑𝑜 𝐶)))
197195, 123, 122, 141, 196syl31anc 1326 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (suc (𝑥𝑧) ⊆ 𝐶 → (ω ↑𝑜 suc (𝑥𝑧)) ⊆ (ω ↑𝑜 𝐶)))
198193, 197mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (ω ↑𝑜 suc (𝑥𝑧)) ⊆ (ω ↑𝑜 𝐶))
199191, 198sstrd 3593 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑𝑜 𝑧))) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶))
200199expr 642 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ 𝑧𝐶) → (𝑦 ∈ (ω ↑𝑜 𝑧) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶)))
201121, 200sylan2 491 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) ∧ 𝑧 ∈ (𝐶 ∖ 1𝑜)) → (𝑦 ∈ (ω ↑𝑜 𝑧) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶)))
202201rexlimdva 3024 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (∃𝑧 ∈ (𝐶 ∖ 1𝑜)𝑦 ∈ (ω ↑𝑜 𝑧) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶)))
203120, 202sylbid 230 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (𝑦 ∈ (ω ↑𝑜 𝐶) → (𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶)))
204203ralrimiv 2959 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → ∀𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶))
205 iunss 4527 . . . . . . . . . . . . . . . . 17 ( 𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶) ↔ ∀𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶))
206204, 205sylibr 224 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → 𝑦 ∈ (ω ↑𝑜 𝐶)(𝐴 +𝑜 𝑦) ⊆ (ω ↑𝑜 𝐶))
207114, 206eqsstrd 3618 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑𝑜 𝑥))) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶))
208207expr 642 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ 𝑥𝐶) → (𝐴 ∈ (ω ↑𝑜 𝑥) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶)))
209101, 208sylan2 491 . . . . . . . . . . . . 13 (((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ 𝑥 ∈ (𝐶 ∖ 1𝑜)) → (𝐴 ∈ (ω ↑𝑜 𝑥) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶)))
210209rexlimdva 3024 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (∃𝑥 ∈ (𝐶 ∖ 1𝑜)𝐴 ∈ (ω ↑𝑜 𝑥) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶)))
211100, 210mpd 15 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) ⊆ (ω ↑𝑜 𝐶))
21288adantr 481 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑𝑜 𝐶) ⊆ (𝐴 +𝑜 (ω ↑𝑜 𝐶)))
213211, 212eqssd 3600 . . . . . . . . . 10 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
214213ex 450 . . . . . . . . 9 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (Lim 𝐶 → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶)))
21543, 91, 2143jaod 1389 . . . . . . . 8 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → ((𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶)))
21628, 215mpd 15 . . . . . . 7 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
217216adantr 481 . . . . . 6 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +𝑜 (ω ↑𝑜 𝐶)) = (ω ↑𝑜 𝐶))
218217oveq1d 6619 . . . . 5 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +𝑜 (ω ↑𝑜 𝐶)) +𝑜 𝑥) = ((ω ↑𝑜 𝐶) +𝑜 𝑥))
21923, 218eqtr3d 2657 . . . 4 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)) = ((ω ↑𝑜 𝐶) +𝑜 𝑥))
220 oveq2 6612 . . . . 5 (((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → (𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)) = (𝐴 +𝑜 𝐵))
221 id 22 . . . . 5 (((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵)
222220, 221eqeq12d 2636 . . . 4 (((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → ((𝐴 +𝑜 ((ω ↑𝑜 𝐶) +𝑜 𝑥)) = ((ω ↑𝑜 𝐶) +𝑜 𝑥) ↔ (𝐴 +𝑜 𝐵) = 𝐵))
223219, 222syl5ibcom 235 . . 3 ((((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → (𝐴 +𝑜 𝐵) = 𝐵))
224223rexlimdva 3024 . 2 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (∃𝑥 ∈ On ((ω ↑𝑜 𝐶) +𝑜 𝑥) = 𝐵 → (𝐴 +𝑜 𝐵) = 𝐵))
22515, 224mpd 15 1 (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐴 +𝑜 𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3o 1035   = wceq 1480  wcel 1987  wral 2907  wrex 2908  ∃!wreu 2909  cdif 3552  cun 3553  wss 3555  c0 3891   ciun 4485   × cxp 5072  dom cdm 5074  Ord word 5681  Oncon0 5682  Lim wlim 5683  suc csuc 5684   Fn wfn 5842  (class class class)co 6604  ωcom 7012  1𝑜c1o 7498  2𝑜c2o 7499   +𝑜 coa 7502   ·𝑜 comu 7503  𝑜 coe 7504
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-omul 7510  df-oexp 7511
This theorem is referenced by:  cnfcomlem  8540
  Copyright terms: Public domain W3C validator