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

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

Proof of Theorem oaabs2
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 n0i 4249 . . . . . . 7 (𝐴 ∈ (ω ↑o 𝐶) → ¬ (ω ↑o 𝐶) = ∅)
2 fnoe 8120 . . . . . . . . 9 o Fn (On × On)
3 fndm 6425 . . . . . . . . 9 ( ↑o Fn (On × On) → dom ↑o = (On × On))
42, 3ax-mp 5 . . . . . . . 8 dom ↑o = (On × On)
54ndmov 7313 . . . . . . 7 (¬ (ω ∈ On ∧ 𝐶 ∈ On) → (ω ↑o 𝐶) = ∅)
61, 5nsyl2 143 . . . . . 6 (𝐴 ∈ (ω ↑o 𝐶) → (ω ∈ On ∧ 𝐶 ∈ On))
76ad2antrr 725 . . . . 5 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → (ω ∈ On ∧ 𝐶 ∈ On))
8 oecl 8147 . . . . 5 ((ω ∈ On ∧ 𝐶 ∈ On) → (ω ↑o 𝐶) ∈ On)
97, 8syl 17 . . . 4 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → (ω ↑o 𝐶) ∈ On)
10 simplr 768 . . . 4 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → 𝐵 ∈ On)
11 simpr 488 . . . 4 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → (ω ↑o 𝐶) ⊆ 𝐵)
12 oawordeu 8166 . . . 4 ((((ω ↑o 𝐶) ∈ On ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → ∃!𝑥 ∈ On ((ω ↑o 𝐶) +o 𝑥) = 𝐵)
139, 10, 11, 12syl21anc 836 . . 3 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → ∃!𝑥 ∈ On ((ω ↑o 𝐶) +o 𝑥) = 𝐵)
14 reurex 3376 . . 3 (∃!𝑥 ∈ On ((ω ↑o 𝐶) +o 𝑥) = 𝐵 → ∃𝑥 ∈ On ((ω ↑o 𝐶) +o 𝑥) = 𝐵)
1513, 14syl 17 . 2 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → ∃𝑥 ∈ On ((ω ↑o 𝐶) +o 𝑥) = 𝐵)
16 simpll 766 . . . . . . . 8 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → 𝐴 ∈ (ω ↑o 𝐶))
17 onelon 6184 . . . . . . . 8 (((ω ↑o 𝐶) ∈ On ∧ 𝐴 ∈ (ω ↑o 𝐶)) → 𝐴 ∈ On)
189, 16, 17syl2anc 587 . . . . . . 7 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → 𝐴 ∈ On)
1918adantr 484 . . . . . 6 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝐴 ∈ On)
209adantr 484 . . . . . 6 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (ω ↑o 𝐶) ∈ On)
21 simpr 488 . . . . . 6 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝑥 ∈ On)
22 oaass 8172 . . . . . 6 ((𝐴 ∈ On ∧ (ω ↑o 𝐶) ∈ On ∧ 𝑥 ∈ On) → ((𝐴 +o (ω ↑o 𝐶)) +o 𝑥) = (𝐴 +o ((ω ↑o 𝐶) +o 𝑥)))
2319, 20, 21, 22syl3anc 1368 . . . . 5 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +o (ω ↑o 𝐶)) +o 𝑥) = (𝐴 +o ((ω ↑o 𝐶) +o 𝑥)))
247simprd 499 . . . . . . . . . 10 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → 𝐶 ∈ On)
25 eloni 6169 . . . . . . . . . 10 (𝐶 ∈ On → Ord 𝐶)
2624, 25syl 17 . . . . . . . . 9 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → Ord 𝐶)
27 ordzsl 7542 . . . . . . . . 9 (Ord 𝐶 ↔ (𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶))
2826, 27sylib 221 . . . . . . . 8 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → (𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶))
29 simplll 774 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 ∈ (ω ↑o 𝐶))
30 oveq2 7143 . . . . . . . . . . . . . . 15 (𝐶 = ∅ → (ω ↑o 𝐶) = (ω ↑o ∅))
317simpld 498 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → ω ∈ On)
32 oe0 8132 . . . . . . . . . . . . . . . 16 (ω ∈ On → (ω ↑o ∅) = 1o)
3331, 32syl 17 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → (ω ↑o ∅) = 1o)
3430, 33sylan9eqr 2855 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (ω ↑o 𝐶) = 1o)
3529, 34eleqtrd 2892 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 ∈ 1o)
36 el1o 8109 . . . . . . . . . . . . 13 (𝐴 ∈ 1o𝐴 = ∅)
3735, 36sylib 221 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 = ∅)
3837oveq1d 7150 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (𝐴 +o (ω ↑o 𝐶)) = (∅ +o (ω ↑o 𝐶)))
399adantr 484 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (ω ↑o 𝐶) ∈ On)
40 oa0r 8148 . . . . . . . . . . . 12 ((ω ↑o 𝐶) ∈ On → (∅ +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
4139, 40syl 17 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (∅ +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
4238, 41eqtrd 2833 . . . . . . . . . 10 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (𝐴 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
4342ex 416 . . . . . . . . 9 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → (𝐶 = ∅ → (𝐴 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶)))
4431adantr 484 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → ω ∈ On)
45 simprl 770 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝑥 ∈ On)
46 oecl 8147 . . . . . . . . . . . . . 14 ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑o 𝑥) ∈ On)
4744, 45, 46syl2anc 587 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑o 𝑥) ∈ On)
48 limom 7577 . . . . . . . . . . . . . 14 Lim ω
4944, 48jctir 524 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ∈ On ∧ Lim ω))
50 simplll 774 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐴 ∈ (ω ↑o 𝐶))
51 simprr 772 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐶 = suc 𝑥)
5251oveq2d 7151 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑o 𝐶) = (ω ↑o suc 𝑥))
53 oesuc 8137 . . . . . . . . . . . . . . . 16 ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑o suc 𝑥) = ((ω ↑o 𝑥) ·o ω))
5444, 45, 53syl2anc 587 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑o suc 𝑥) = ((ω ↑o 𝑥) ·o ω))
5552, 54eqtrd 2833 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑o 𝐶) = ((ω ↑o 𝑥) ·o ω))
5650, 55eleqtrd 2892 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐴 ∈ ((ω ↑o 𝑥) ·o ω))
57 omordlim 8188 . . . . . . . . . . . . 13 ((((ω ↑o 𝑥) ∈ On ∧ (ω ∈ On ∧ Lim ω)) ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o ω)) → ∃𝑦 ∈ ω 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))
5847, 49, 56, 57syl21anc 836 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → ∃𝑦 ∈ ω 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))
5947adantr 484 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (ω ↑o 𝑥) ∈ On)
60 nnon 7568 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ω → 𝑦 ∈ On)
6160ad2antrl 727 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → 𝑦 ∈ On)
62 omcl 8146 . . . . . . . . . . . . . . . . 17 (((ω ↑o 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω ↑o 𝑥) ·o 𝑦) ∈ On)
6359, 61, 62syl2anc 587 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → ((ω ↑o 𝑥) ·o 𝑦) ∈ On)
64 eloni 6169 . . . . . . . . . . . . . . . 16 (((ω ↑o 𝑥) ·o 𝑦) ∈ On → Ord ((ω ↑o 𝑥) ·o 𝑦))
6563, 64syl 17 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → Ord ((ω ↑o 𝑥) ·o 𝑦))
66 simprr 772 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))
67 ordelss 6175 . . . . . . . . . . . . . . 15 ((Ord ((ω ↑o 𝑥) ·o 𝑦) ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦)) → 𝐴 ⊆ ((ω ↑o 𝑥) ·o 𝑦))
6865, 66, 67syl2anc 587 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → 𝐴 ⊆ ((ω ↑o 𝑥) ·o 𝑦))
6918ad2antrr 725 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → 𝐴 ∈ On)
709ad2antrr 725 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (ω ↑o 𝐶) ∈ On)
71 oawordri 8161 . . . . . . . . . . . . . . 15 ((𝐴 ∈ On ∧ ((ω ↑o 𝑥) ·o 𝑦) ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (𝐴 ⊆ ((ω ↑o 𝑥) ·o 𝑦) → (𝐴 +o (ω ↑o 𝐶)) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝐶))))
7269, 63, 70, 71syl3anc 1368 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (𝐴 ⊆ ((ω ↑o 𝑥) ·o 𝑦) → (𝐴 +o (ω ↑o 𝐶)) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝐶))))
7368, 72mpd 15 . . . . . . . . . . . . 13 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (𝐴 +o (ω ↑o 𝐶)) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝐶)))
7444adantr 484 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → ω ∈ On)
75 odi 8190 . . . . . . . . . . . . . . . 16 (((ω ↑o 𝑥) ∈ On ∧ 𝑦 ∈ On ∧ ω ∈ On) → ((ω ↑o 𝑥) ·o (𝑦 +o ω)) = (((ω ↑o 𝑥) ·o 𝑦) +o ((ω ↑o 𝑥) ·o ω)))
7659, 61, 74, 75syl3anc 1368 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → ((ω ↑o 𝑥) ·o (𝑦 +o ω)) = (((ω ↑o 𝑥) ·o 𝑦) +o ((ω ↑o 𝑥) ·o ω)))
77 simprl 770 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → 𝑦 ∈ ω)
78 oaabslem 8255 . . . . . . . . . . . . . . . . 17 ((ω ∈ On ∧ 𝑦 ∈ ω) → (𝑦 +o ω) = ω)
7974, 77, 78syl2anc 587 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (𝑦 +o ω) = ω)
8079oveq2d 7151 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → ((ω ↑o 𝑥) ·o (𝑦 +o ω)) = ((ω ↑o 𝑥) ·o ω))
8176, 80eqtr3d 2835 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (((ω ↑o 𝑥) ·o 𝑦) +o ((ω ↑o 𝑥) ·o ω)) = ((ω ↑o 𝑥) ·o ω))
8255adantr 484 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (ω ↑o 𝐶) = ((ω ↑o 𝑥) ·o ω))
8382oveq2d 7151 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝐶)) = (((ω ↑o 𝑥) ·o 𝑦) +o ((ω ↑o 𝑥) ·o ω)))
8481, 83, 823eqtr4d 2843 . . . . . . . . . . . . 13 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
8573, 84sseqtrd 3955 . . . . . . . . . . . 12 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑o 𝑥) ·o 𝑦))) → (𝐴 +o (ω ↑o 𝐶)) ⊆ (ω ↑o 𝐶))
8658, 85rexlimddv 3250 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (𝐴 +o (ω ↑o 𝐶)) ⊆ (ω ↑o 𝐶))
87 oaword2 8164 . . . . . . . . . . . . 13 (((ω ↑o 𝐶) ∈ On ∧ 𝐴 ∈ On) → (ω ↑o 𝐶) ⊆ (𝐴 +o (ω ↑o 𝐶)))
889, 18, 87syl2anc 587 . . . . . . . . . . . 12 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → (ω ↑o 𝐶) ⊆ (𝐴 +o (ω ↑o 𝐶)))
8988adantr 484 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑o 𝐶) ⊆ (𝐴 +o (ω ↑o 𝐶)))
9086, 89eqssd 3932 . . . . . . . . . 10 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (𝐴 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
9190rexlimdvaa 3244 . . . . . . . . 9 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → (∃𝑥 ∈ On 𝐶 = suc 𝑥 → (𝐴 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶)))
92 simplll 774 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐴 ∈ (ω ↑o 𝐶))
9331adantr 484 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → ω ∈ On)
9424adantr 484 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐶 ∈ On)
95 simpr 488 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → Lim 𝐶)
96 oelim2 8206 . . . . . . . . . . . . . . 15 ((ω ∈ On ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → (ω ↑o 𝐶) = 𝑥 ∈ (𝐶 ∖ 1o)(ω ↑o 𝑥))
9793, 94, 95, 96syl12anc 835 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑o 𝐶) = 𝑥 ∈ (𝐶 ∖ 1o)(ω ↑o 𝑥))
9892, 97eleqtrd 2892 . . . . . . . . . . . . 13 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐴 𝑥 ∈ (𝐶 ∖ 1o)(ω ↑o 𝑥))
99 eliun 4885 . . . . . . . . . . . . 13 (𝐴 𝑥 ∈ (𝐶 ∖ 1o)(ω ↑o 𝑥) ↔ ∃𝑥 ∈ (𝐶 ∖ 1o)𝐴 ∈ (ω ↑o 𝑥))
10098, 99sylib 221 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → ∃𝑥 ∈ (𝐶 ∖ 1o)𝐴 ∈ (ω ↑o 𝑥))
101 eldifi 4054 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐶 ∖ 1o) → 𝑥𝐶)
10218ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) → 𝐴 ∈ On)
1039ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) → (ω ↑o 𝐶) ∈ On)
10493adantr 484 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) → ω ∈ On)
105 1onn 8250 . . . . . . . . . . . . . . . . . . 19 1o ∈ ω
106 ondif2 8112 . . . . . . . . . . . . . . . . . . 19 (ω ∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o ∈ ω))
107104, 105, 106sylanblrc 593 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) → ω ∈ (On ∖ 2o))
10894adantr 484 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) → 𝐶 ∈ On)
109 simplr 768 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) → Lim 𝐶)
110 oelimcl 8211 . . . . . . . . . . . . . . . . . 18 ((ω ∈ (On ∖ 2o) ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → Lim (ω ↑o 𝐶))
111107, 108, 109, 110syl12anc 835 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) → Lim (ω ↑o 𝐶))
112 oalim 8142 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ ((ω ↑o 𝐶) ∈ On ∧ Lim (ω ↑o 𝐶))) → (𝐴 +o (ω ↑o 𝐶)) = 𝑦 ∈ (ω ↑o 𝐶)(𝐴 +o 𝑦))
113102, 103, 111, 112syl12anc 835 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) → (𝐴 +o (ω ↑o 𝐶)) = 𝑦 ∈ (ω ↑o 𝐶)(𝐴 +o 𝑦))
114 oelim2 8206 . . . . . . . . . . . . . . . . . . . . . . 23 ((ω ∈ On ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → (ω ↑o 𝐶) = 𝑧 ∈ (𝐶 ∖ 1o)(ω ↑o 𝑧))
11593, 94, 95, 114syl12anc 835 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑o 𝐶) = 𝑧 ∈ (𝐶 ∖ 1o)(ω ↑o 𝑧))
116115eleq2d 2875 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝑦 ∈ (ω ↑o 𝐶) ↔ 𝑦 𝑧 ∈ (𝐶 ∖ 1o)(ω ↑o 𝑧)))
117 eliun 4885 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 𝑧 ∈ (𝐶 ∖ 1o)(ω ↑o 𝑧) ↔ ∃𝑧 ∈ (𝐶 ∖ 1o)𝑦 ∈ (ω ↑o 𝑧))
118116, 117syl6bb 290 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝑦 ∈ (ω ↑o 𝐶) ↔ ∃𝑧 ∈ (𝐶 ∖ 1o)𝑦 ∈ (ω ↑o 𝑧)))
119118adantr 484 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) → (𝑦 ∈ (ω ↑o 𝐶) ↔ ∃𝑧 ∈ (𝐶 ∖ 1o)𝑦 ∈ (ω ↑o 𝑧)))
120 eldifi 4054 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ (𝐶 ∖ 1o) → 𝑧𝐶)
121104adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → ω ∈ On)
122108adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → 𝐶 ∈ On)
123 simplrl 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → 𝑥𝐶)
124 onelon 6184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐶 ∈ On ∧ 𝑥𝐶) → 𝑥 ∈ On)
125122, 123, 124syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → 𝑥 ∈ On)
126121, 125, 46syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (ω ↑o 𝑥) ∈ On)
127 eloni 6169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ω ↑o 𝑥) ∈ On → Ord (ω ↑o 𝑥))
128126, 127syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → Ord (ω ↑o 𝑥))
129 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → 𝐴 ∈ (ω ↑o 𝑥))
130 ordelss 6175 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Ord (ω ↑o 𝑥) ∧ 𝐴 ∈ (ω ↑o 𝑥)) → 𝐴 ⊆ (ω ↑o 𝑥))
131128, 129, 130syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → 𝐴 ⊆ (ω ↑o 𝑥))
132 ssun1 4099 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑥 ⊆ (𝑥𝑧)
13326ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → Ord 𝐶)
134 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → 𝑧𝐶)
135 ordunel 7524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((Ord 𝐶𝑥𝐶𝑧𝐶) → (𝑥𝑧) ∈ 𝐶)
136133, 123, 134, 135syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (𝑥𝑧) ∈ 𝐶)
137 onelon 6184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐶 ∈ On ∧ (𝑥𝑧) ∈ 𝐶) → (𝑥𝑧) ∈ On)
138122, 136, 137syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (𝑥𝑧) ∈ On)
139 peano1 7583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ ∈ ω
140139a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → ∅ ∈ ω)
141 oewordi 8202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 ∈ On ∧ (𝑥𝑧) ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (𝑥 ⊆ (𝑥𝑧) → (ω ↑o 𝑥) ⊆ (ω ↑o (𝑥𝑧))))
142125, 138, 121, 140, 141syl31anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (𝑥 ⊆ (𝑥𝑧) → (ω ↑o 𝑥) ⊆ (ω ↑o (𝑥𝑧))))
143132, 142mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (ω ↑o 𝑥) ⊆ (ω ↑o (𝑥𝑧)))
144131, 143sstrd 3925 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → 𝐴 ⊆ (ω ↑o (𝑥𝑧)))
145102adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → 𝐴 ∈ On)
146 oecl 8147 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ω ∈ On ∧ (𝑥𝑧) ∈ On) → (ω ↑o (𝑥𝑧)) ∈ On)
147121, 138, 146syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (ω ↑o (𝑥𝑧)) ∈ On)
148 onelon 6184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐶 ∈ On ∧ 𝑧𝐶) → 𝑧 ∈ On)
149122, 134, 148syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → 𝑧 ∈ On)
150 oecl 8147 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ω ∈ On ∧ 𝑧 ∈ On) → (ω ↑o 𝑧) ∈ On)
151121, 149, 150syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (ω ↑o 𝑧) ∈ On)
152 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → 𝑦 ∈ (ω ↑o 𝑧))
153 onelon 6184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ω ↑o 𝑧) ∈ On ∧ 𝑦 ∈ (ω ↑o 𝑧)) → 𝑦 ∈ On)
154151, 152, 153syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → 𝑦 ∈ On)
155 oawordri 8161 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ On ∧ (ω ↑o (𝑥𝑧)) ∈ On ∧ 𝑦 ∈ On) → (𝐴 ⊆ (ω ↑o (𝑥𝑧)) → (𝐴 +o 𝑦) ⊆ ((ω ↑o (𝑥𝑧)) +o 𝑦)))
156145, 147, 154, 155syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (𝐴 ⊆ (ω ↑o (𝑥𝑧)) → (𝐴 +o 𝑦) ⊆ ((ω ↑o (𝑥𝑧)) +o 𝑦)))
157144, 156mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (𝐴 +o 𝑦) ⊆ ((ω ↑o (𝑥𝑧)) +o 𝑦))
158 eloni 6169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((ω ↑o 𝑧) ∈ On → Ord (ω ↑o 𝑧))
159151, 158syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → Ord (ω ↑o 𝑧))
160 ordelss 6175 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Ord (ω ↑o 𝑧) ∧ 𝑦 ∈ (ω ↑o 𝑧)) → 𝑦 ⊆ (ω ↑o 𝑧))
161159, 152, 160syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → 𝑦 ⊆ (ω ↑o 𝑧))
162 ssun2 4100 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑧 ⊆ (𝑥𝑧)
163 oewordi 8202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑧 ∈ On ∧ (𝑥𝑧) ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (𝑧 ⊆ (𝑥𝑧) → (ω ↑o 𝑧) ⊆ (ω ↑o (𝑥𝑧))))
164149, 138, 121, 140, 163syl31anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (𝑧 ⊆ (𝑥𝑧) → (ω ↑o 𝑧) ⊆ (ω ↑o (𝑥𝑧))))
165162, 164mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (ω ↑o 𝑧) ⊆ (ω ↑o (𝑥𝑧)))
166161, 165sstrd 3925 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → 𝑦 ⊆ (ω ↑o (𝑥𝑧)))
167 oaword 8160 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ On ∧ (ω ↑o (𝑥𝑧)) ∈ On ∧ (ω ↑o (𝑥𝑧)) ∈ On) → (𝑦 ⊆ (ω ↑o (𝑥𝑧)) ↔ ((ω ↑o (𝑥𝑧)) +o 𝑦) ⊆ ((ω ↑o (𝑥𝑧)) +o (ω ↑o (𝑥𝑧)))))
168154, 147, 147, 167syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (𝑦 ⊆ (ω ↑o (𝑥𝑧)) ↔ ((ω ↑o (𝑥𝑧)) +o 𝑦) ⊆ ((ω ↑o (𝑥𝑧)) +o (ω ↑o (𝑥𝑧)))))
169166, 168mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → ((ω ↑o (𝑥𝑧)) +o 𝑦) ⊆ ((ω ↑o (𝑥𝑧)) +o (ω ↑o (𝑥𝑧))))
170157, 169sstrd 3925 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (𝐴 +o 𝑦) ⊆ ((ω ↑o (𝑥𝑧)) +o (ω ↑o (𝑥𝑧))))
171 ordom 7571 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ord ω
172 ordsucss 7515 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Ord ω → (1o ∈ ω → suc 1o ⊆ ω))
173171, 105, 172mp2 9 . . . . . . . . . . . . . . . . . . . . . . . . . 26 suc 1o ⊆ ω
174 1on 8094 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1o ∈ On
175 suceloni 7510 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1o ∈ On → suc 1o ∈ On)
176174, 175mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → suc 1o ∈ On)
177 omwordi 8182 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((suc 1o ∈ On ∧ ω ∈ On ∧ (ω ↑o (𝑥𝑧)) ∈ On) → (suc 1o ⊆ ω → ((ω ↑o (𝑥𝑧)) ·o suc 1o) ⊆ ((ω ↑o (𝑥𝑧)) ·o ω)))
178176, 121, 147, 177syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (suc 1o ⊆ ω → ((ω ↑o (𝑥𝑧)) ·o suc 1o) ⊆ ((ω ↑o (𝑥𝑧)) ·o ω)))
179173, 178mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → ((ω ↑o (𝑥𝑧)) ·o suc 1o) ⊆ ((ω ↑o (𝑥𝑧)) ·o ω))
180174a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → 1o ∈ On)
181 omsuc 8136 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((ω ↑o (𝑥𝑧)) ∈ On ∧ 1o ∈ On) → ((ω ↑o (𝑥𝑧)) ·o suc 1o) = (((ω ↑o (𝑥𝑧)) ·o 1o) +o (ω ↑o (𝑥𝑧))))
182147, 180, 181syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → ((ω ↑o (𝑥𝑧)) ·o suc 1o) = (((ω ↑o (𝑥𝑧)) ·o 1o) +o (ω ↑o (𝑥𝑧))))
183 om1 8153 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ω ↑o (𝑥𝑧)) ∈ On → ((ω ↑o (𝑥𝑧)) ·o 1o) = (ω ↑o (𝑥𝑧)))
184147, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → ((ω ↑o (𝑥𝑧)) ·o 1o) = (ω ↑o (𝑥𝑧)))
185184oveq1d 7150 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (((ω ↑o (𝑥𝑧)) ·o 1o) +o (ω ↑o (𝑥𝑧))) = ((ω ↑o (𝑥𝑧)) +o (ω ↑o (𝑥𝑧))))
186182, 185eqtr2d 2834 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → ((ω ↑o (𝑥𝑧)) +o (ω ↑o (𝑥𝑧))) = ((ω ↑o (𝑥𝑧)) ·o suc 1o))
187 oesuc 8137 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ω ∈ On ∧ (𝑥𝑧) ∈ On) → (ω ↑o suc (𝑥𝑧)) = ((ω ↑o (𝑥𝑧)) ·o ω))
188121, 138, 187syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (ω ↑o suc (𝑥𝑧)) = ((ω ↑o (𝑥𝑧)) ·o ω))
189179, 186, 1883sstr4d 3962 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → ((ω ↑o (𝑥𝑧)) +o (ω ↑o (𝑥𝑧))) ⊆ (ω ↑o suc (𝑥𝑧)))
190170, 189sstrd 3925 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (𝐴 +o 𝑦) ⊆ (ω ↑o suc (𝑥𝑧)))
191 ordsucss 7515 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord 𝐶 → ((𝑥𝑧) ∈ 𝐶 → suc (𝑥𝑧) ⊆ 𝐶))
192133, 136, 191sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → suc (𝑥𝑧) ⊆ 𝐶)
193 suceloni 7510 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥𝑧) ∈ On → suc (𝑥𝑧) ∈ On)
194138, 193syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → suc (𝑥𝑧) ∈ On)
195 oewordi 8202 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((suc (𝑥𝑧) ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (suc (𝑥𝑧) ⊆ 𝐶 → (ω ↑o suc (𝑥𝑧)) ⊆ (ω ↑o 𝐶)))
196194, 122, 121, 140, 195syl31anc 1370 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (suc (𝑥𝑧) ⊆ 𝐶 → (ω ↑o suc (𝑥𝑧)) ⊆ (ω ↑o 𝐶)))
197192, 196mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (ω ↑o suc (𝑥𝑧)) ⊆ (ω ↑o 𝐶))
198190, 197sstrd 3925 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ (𝑧𝐶𝑦 ∈ (ω ↑o 𝑧))) → (𝐴 +o 𝑦) ⊆ (ω ↑o 𝐶))
199198expr 460 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ 𝑧𝐶) → (𝑦 ∈ (ω ↑o 𝑧) → (𝐴 +o 𝑦) ⊆ (ω ↑o 𝐶)))
200120, 199sylan2 595 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) ∧ 𝑧 ∈ (𝐶 ∖ 1o)) → (𝑦 ∈ (ω ↑o 𝑧) → (𝐴 +o 𝑦) ⊆ (ω ↑o 𝐶)))
201200rexlimdva 3243 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) → (∃𝑧 ∈ (𝐶 ∖ 1o)𝑦 ∈ (ω ↑o 𝑧) → (𝐴 +o 𝑦) ⊆ (ω ↑o 𝐶)))
202119, 201sylbid 243 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) → (𝑦 ∈ (ω ↑o 𝐶) → (𝐴 +o 𝑦) ⊆ (ω ↑o 𝐶)))
203202ralrimiv 3148 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) → ∀𝑦 ∈ (ω ↑o 𝐶)(𝐴 +o 𝑦) ⊆ (ω ↑o 𝐶))
204 iunss 4932 . . . . . . . . . . . . . . . . 17 ( 𝑦 ∈ (ω ↑o 𝐶)(𝐴 +o 𝑦) ⊆ (ω ↑o 𝐶) ↔ ∀𝑦 ∈ (ω ↑o 𝐶)(𝐴 +o 𝑦) ⊆ (ω ↑o 𝐶))
205203, 204sylibr 237 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) → 𝑦 ∈ (ω ↑o 𝐶)(𝐴 +o 𝑦) ⊆ (ω ↑o 𝐶))
206113, 205eqsstrd 3953 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥𝐶𝐴 ∈ (ω ↑o 𝑥))) → (𝐴 +o (ω ↑o 𝐶)) ⊆ (ω ↑o 𝐶))
207206expr 460 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ 𝑥𝐶) → (𝐴 ∈ (ω ↑o 𝑥) → (𝐴 +o (ω ↑o 𝐶)) ⊆ (ω ↑o 𝐶)))
208101, 207sylan2 595 . . . . . . . . . . . . 13 (((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ 𝑥 ∈ (𝐶 ∖ 1o)) → (𝐴 ∈ (ω ↑o 𝑥) → (𝐴 +o (ω ↑o 𝐶)) ⊆ (ω ↑o 𝐶)))
209208rexlimdva 3243 . . . . . . . . . . . 12 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (∃𝑥 ∈ (𝐶 ∖ 1o)𝐴 ∈ (ω ↑o 𝑥) → (𝐴 +o (ω ↑o 𝐶)) ⊆ (ω ↑o 𝐶)))
210100, 209mpd 15 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝐴 +o (ω ↑o 𝐶)) ⊆ (ω ↑o 𝐶))
21188adantr 484 . . . . . . . . . . 11 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑o 𝐶) ⊆ (𝐴 +o (ω ↑o 𝐶)))
212210, 211eqssd 3932 . . . . . . . . . 10 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝐴 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
213212ex 416 . . . . . . . . 9 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → (Lim 𝐶 → (𝐴 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶)))
21443, 91, 2133jaod 1425 . . . . . . . 8 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → ((𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶) → (𝐴 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶)))
21528, 214mpd 15 . . . . . . 7 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → (𝐴 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
216215adantr 484 . . . . . 6 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
217216oveq1d 7150 . . . . 5 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +o (ω ↑o 𝐶)) +o 𝑥) = ((ω ↑o 𝐶) +o 𝑥))
21823, 217eqtr3d 2835 . . . 4 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +o ((ω ↑o 𝐶) +o 𝑥)) = ((ω ↑o 𝐶) +o 𝑥))
219 oveq2 7143 . . . . 5 (((ω ↑o 𝐶) +o 𝑥) = 𝐵 → (𝐴 +o ((ω ↑o 𝐶) +o 𝑥)) = (𝐴 +o 𝐵))
220 id 22 . . . . 5 (((ω ↑o 𝐶) +o 𝑥) = 𝐵 → ((ω ↑o 𝐶) +o 𝑥) = 𝐵)
221219, 220eqeq12d 2814 . . . 4 (((ω ↑o 𝐶) +o 𝑥) = 𝐵 → ((𝐴 +o ((ω ↑o 𝐶) +o 𝑥)) = ((ω ↑o 𝐶) +o 𝑥) ↔ (𝐴 +o 𝐵) = 𝐵))
222218, 221syl5ibcom 248 . . 3 ((((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (((ω ↑o 𝐶) +o 𝑥) = 𝐵 → (𝐴 +o 𝐵) = 𝐵))
223222rexlimdva 3243 . 2 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → (∃𝑥 ∈ On ((ω ↑o 𝐶) +o 𝑥) = 𝐵 → (𝐴 +o 𝐵) = 𝐵))
22415, 223mpd 15 1 (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → (𝐴 +o 𝐵) = 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ w3o 1083   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107  ∃!wreu 3108   ∖ cdif 3878   ∪ cun 3879   ⊆ wss 3881  ∅c0 4243  ∪ ciun 4881   × cxp 5517  dom cdm 5519  Ord word 6158  Oncon0 6159  Lim wlim 6160  suc csuc 6161   Fn wfn 6319  (class class class)co 7135  ωcom 7562  1oc1o 8080  2oc2o 8081   +o coa 8084   ·o comu 8085   ↑o coe 8086 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7563  df-1st 7673  df-2nd 7674  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-1o 8087  df-2o 8088  df-oadd 8091  df-omul 8092  df-oexp 8093 This theorem is referenced by:  cnfcomlem  9148
 Copyright terms: Public domain W3C validator