This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oaabs2

Description: The absorption law oaabs is also a property of higher powers of _om . (Contributed by Mario Carneiro, 29-May-2015)

Ref Expression
Assertion oaabs2 ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( 𝐴 +o 𝐵 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 n0i ⊢ ( 𝐴 ∈ ( ω ↑o 𝐶 ) → ¬ ( ω ↑o 𝐶 ) = ∅ )
2 fnoe ⊢ ↑o Fn ( On × On )
3 fndm ⊢ ( ↑o Fn ( On × On ) → dom ↑o = ( On × On ) )
4 2 3 ax-mp ⊢ dom ↑o = ( On × On )
5 4 ndmov ⊢ ( ¬ ( ω ∈ On ∧ 𝐶 ∈ On ) → ( ω ↑o 𝐶 ) = ∅ )
6 1 5 nsyl2 ⊢ ( 𝐴 ∈ ( ω ↑o 𝐶 ) → ( ω ∈ On ∧ 𝐶 ∈ On ) )
7 6 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ω ∈ On ∧ 𝐶 ∈ On ) )
8 oecl ⊢ ( ( ω ∈ On ∧ 𝐶 ∈ On ) → ( ω ↑o 𝐶 ) ∈ On )
9 7 8 syl ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ω ↑o 𝐶 ) ∈ On )
10 simplr ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → 𝐵 ∈ On )
11 simpr ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ω ↑o 𝐶 ) ⊆ 𝐵 )
12 oawordeu ⊢ ( ( ( ( ω ↑o 𝐶 ) ∈ On ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ∃! 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 )
13 9 10 11 12 syl21anc ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ∃! 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 )
14 reurex ⊢ ( ∃! 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ∃ 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 )
15 13 14 syl ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ∃ 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 )
16 simpll ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → 𝐴 ∈ ( ω ↑o 𝐶 ) )
17 onelon ⊢ ( ( ( ω ↑o 𝐶 ) ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝐶 ) ) → 𝐴 ∈ On )
18 9 16 17 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → 𝐴 ∈ On )
19 18 adantr ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → 𝐴 ∈ On )
20 9 adantr ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( ω ↑o 𝐶 ) ∈ On )
21 simpr ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → 𝑥 ∈ On )
22 oaass ⊢ ( ( 𝐴 ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ∧ 𝑥 ∈ On ) → ( ( 𝐴 +o ( ω ↑o 𝐶 ) ) +o 𝑥 ) = ( 𝐴 +o ( ( ω ↑o 𝐶 ) +o 𝑥 ) ) )
23 19 20 21 22 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( ( 𝐴 +o ( ω ↑o 𝐶 ) ) +o 𝑥 ) = ( 𝐴 +o ( ( ω ↑o 𝐶 ) +o 𝑥 ) ) )
24 7 simprd ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → 𝐶 ∈ On )
25 eloni ⊢ ( 𝐶 ∈ On → Ord 𝐶 )
26 24 25 syl ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → Ord 𝐶 )
27 ordzsl ⊢ ( Ord 𝐶 ↔ ( 𝐶 = ∅ ∨ ∃ 𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶 ) )
28 26 27 sylib ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( 𝐶 = ∅ ∨ ∃ 𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶 ) )
29 simplll ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → 𝐴 ∈ ( ω ↑o 𝐶 ) )
30 oveq2 ⊢ ( 𝐶 = ∅ → ( ω ↑o 𝐶 ) = ( ω ↑o ∅ ) )
31 7 simpld ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ω ∈ On )
32 oe0 ⊢ ( ω ∈ On → ( ω ↑o ∅ ) = 1o )
33 31 32 syl ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ω ↑o ∅ ) = 1o )
34 30 33 sylan9eqr ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → ( ω ↑o 𝐶 ) = 1o )
35 29 34 eleqtrd ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → 𝐴 ∈ 1o )
36 el1o ⊢ ( 𝐴 ∈ 1o ↔ 𝐴 = ∅ )
37 35 36 sylib ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → 𝐴 = ∅ )
38 37 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ∅ +o ( ω ↑o 𝐶 ) ) )
39 9 adantr ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → ( ω ↑o 𝐶 ) ∈ On )
40 oa0r ⊢ ( ( ω ↑o 𝐶 ) ∈ On → ( ∅ +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
41 39 40 syl ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → ( ∅ +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
42 38 41 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
43 42 ex ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( 𝐶 = ∅ → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) )
44 31 adantr ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ω ∈ On )
45 simprl ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → 𝑥 ∈ On )
46 oecl ⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ) → ( ω ↑o 𝑥 ) ∈ On )
47 44 45 46 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ↑o 𝑥 ) ∈ On )
48 limom ⊢ Lim ω
49 44 48 jctir ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ∈ On ∧ Lim ω ) )
50 simplll ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → 𝐴 ∈ ( ω ↑o 𝐶 ) )
51 simprr ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → 𝐶 = suc 𝑥 )
52 51 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ↑o 𝐶 ) = ( ω ↑o suc 𝑥 ) )
53 oesuc ⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ) → ( ω ↑o suc 𝑥 ) = ( ( ω ↑o 𝑥 ) ·o ω ) )
54 44 45 53 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ↑o suc 𝑥 ) = ( ( ω ↑o 𝑥 ) ·o ω ) )
55 52 54 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ↑o 𝐶 ) = ( ( ω ↑o 𝑥 ) ·o ω ) )
56 50 55 eleqtrd ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o ω ) )
57 omordlim ⊢ ( ( ( ( ω ↑o 𝑥 ) ∈ On ∧ ( ω ∈ On ∧ Lim ω ) ) ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o ω ) ) → ∃ 𝑦 ∈ ω 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) )
58 47 49 56 57 syl21anc ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ∃ 𝑦 ∈ ω 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) )
59 47 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ω ↑o 𝑥 ) ∈ On )
60 nnon ⊢ ( 𝑦 ∈ ω → 𝑦 ∈ On )
61 60 ad2antrl ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → 𝑦 ∈ On )
62 omcl ⊢ ( ( ( ω ↑o 𝑥 ) ∈ On ∧ 𝑦 ∈ On ) → ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∈ On )
63 59 61 62 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∈ On )
64 eloni ⊢ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∈ On → Ord ( ( ω ↑o 𝑥 ) ·o 𝑦 ) )
65 63 64 syl ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → Ord ( ( ω ↑o 𝑥 ) ·o 𝑦 ) )
66 simprr ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) )
67 ordelss ⊢ ( ( Ord ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) → 𝐴 ⊆ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) )
68 65 66 67 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → 𝐴 ⊆ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) )
69 18 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → 𝐴 ∈ On )
70 9 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ω ↑o 𝐶 ) ∈ On )
71 oawordri ⊢ ( ( 𝐴 ∈ On ∧ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ) → ( 𝐴 ⊆ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝐶 ) ) ) )
72 69 63 70 71 syl3anc ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( 𝐴 ⊆ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝐶 ) ) ) )
73 68 72 mpd ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝐶 ) ) )
74 44 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ω ∈ On )
75 odi ⊢ ( ( ( ω ↑o 𝑥 ) ∈ On ∧ 𝑦 ∈ On ∧ ω ∈ On ) → ( ( ω ↑o 𝑥 ) ·o ( 𝑦 +o ω ) ) = ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ( ω ↑o 𝑥 ) ·o ω ) ) )
76 59 61 74 75 syl3anc ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ω ↑o 𝑥 ) ·o ( 𝑦 +o ω ) ) = ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ( ω ↑o 𝑥 ) ·o ω ) ) )
77 simprl ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → 𝑦 ∈ ω )
78 oaabslem ⊢ ( ( ω ∈ On ∧ 𝑦 ∈ ω ) → ( 𝑦 +o ω ) = ω )
79 74 77 78 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( 𝑦 +o ω ) = ω )
80 79 oveq2d ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ω ↑o 𝑥 ) ·o ( 𝑦 +o ω ) ) = ( ( ω ↑o 𝑥 ) ·o ω ) )
81 76 80 eqtr3d ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ( ω ↑o 𝑥 ) ·o ω ) ) = ( ( ω ↑o 𝑥 ) ·o ω ) )
82 55 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ω ↑o 𝐶 ) = ( ( ω ↑o 𝑥 ) ·o ω ) )
83 82 oveq2d ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝐶 ) ) = ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ( ω ↑o 𝑥 ) ·o ω ) ) )
84 81 83 82 3eqtr4d ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
85 73 84 sseqtrd ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) )
86 58 85 rexlimddv ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) )
87 oaword2 ⊢ ( ( ( ω ↑o 𝐶 ) ∈ On ∧ 𝐴 ∈ On ) → ( ω ↑o 𝐶 ) ⊆ ( 𝐴 +o ( ω ↑o 𝐶 ) ) )
88 9 18 87 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ω ↑o 𝐶 ) ⊆ ( 𝐴 +o ( ω ↑o 𝐶 ) ) )
89 88 adantr ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ↑o 𝐶 ) ⊆ ( 𝐴 +o ( ω ↑o 𝐶 ) ) )
90 86 89 eqssd ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
91 90 rexlimdvaa ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ∃ 𝑥 ∈ On 𝐶 = suc 𝑥 → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) )
92 simplll ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → 𝐴 ∈ ( ω ↑o 𝐶 ) )
93 31 adantr ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ω ∈ On )
94 24 adantr ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → 𝐶 ∈ On )
95 simpr ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → Lim 𝐶 )
96 oelim2 ⊢ ( ( ω ∈ On ∧ ( 𝐶 ∈ On ∧ Lim 𝐶 ) ) → ( ω ↑o 𝐶 ) = ∪ 𝑥 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑥 ) )
97 93 94 95 96 syl12anc ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( ω ↑o 𝐶 ) = ∪ 𝑥 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑥 ) )
98 92 97 eleqtrd ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → 𝐴 ∈ ∪ 𝑥 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑥 ) )
99 eliun ⊢ ( 𝐴 ∈ ∪ 𝑥 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑥 ) ↔ ∃ 𝑥 ∈ ( 𝐶 ∖ 1o ) 𝐴 ∈ ( ω ↑o 𝑥 ) )
100 98 99 sylib ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ∃ 𝑥 ∈ ( 𝐶 ∖ 1o ) 𝐴 ∈ ( ω ↑o 𝑥 ) )
101 eldifi ⊢ ( 𝑥 ∈ ( 𝐶 ∖ 1o ) → 𝑥 ∈ 𝐶 )
102 18 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → 𝐴 ∈ On )
103 9 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( ω ↑o 𝐶 ) ∈ On )
104 93 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ω ∈ On )
105 1onn ⊢ 1o ∈ ω
106 ondif2 ⊢ ( ω ∈ ( On ∖ 2o ) ↔ ( ω ∈ On ∧ 1o ∈ ω ) )
107 104 105 106 sylanblrc ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ω ∈ ( On ∖ 2o ) )
108 94 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → 𝐶 ∈ On )
109 simplr ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → Lim 𝐶 )
110 oelimcl ⊢ ( ( ω ∈ ( On ∖ 2o ) ∧ ( 𝐶 ∈ On ∧ Lim 𝐶 ) ) → Lim ( ω ↑o 𝐶 ) )
111 107 108 109 110 syl12anc ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → Lim ( ω ↑o 𝐶 ) )
112 oalim ⊢ ( ( 𝐴 ∈ On ∧ ( ( ω ↑o 𝐶 ) ∈ On ∧ Lim ( ω ↑o 𝐶 ) ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ∪ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) )
113 102 103 111 112 syl12anc ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ∪ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) )
114 oelim2 ⊢ ( ( ω ∈ On ∧ ( 𝐶 ∈ On ∧ Lim 𝐶 ) ) → ( ω ↑o 𝐶 ) = ∪ 𝑧 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑧 ) )
115 93 94 95 114 syl12anc ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( ω ↑o 𝐶 ) = ∪ 𝑧 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑧 ) )
116 115 eleq2d ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( 𝑦 ∈ ( ω ↑o 𝐶 ) ↔ 𝑦 ∈ ∪ 𝑧 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑧 ) ) )
117 eliun ⊢ ( 𝑦 ∈ ∪ 𝑧 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑧 ) ↔ ∃ 𝑧 ∈ ( 𝐶 ∖ 1o ) 𝑦 ∈ ( ω ↑o 𝑧 ) )
118 116 117 bitrdi ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( 𝑦 ∈ ( ω ↑o 𝐶 ) ↔ ∃ 𝑧 ∈ ( 𝐶 ∖ 1o ) 𝑦 ∈ ( ω ↑o 𝑧 ) ) )
119 118 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( 𝑦 ∈ ( ω ↑o 𝐶 ) ↔ ∃ 𝑧 ∈ ( 𝐶 ∖ 1o ) 𝑦 ∈ ( ω ↑o 𝑧 ) ) )
120 eldifi ⊢ ( 𝑧 ∈ ( 𝐶 ∖ 1o ) → 𝑧 ∈ 𝐶 )
121 104 adantr ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ω ∈ On )
122 108 adantr ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝐶 ∈ On )
123 simplrl ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑥 ∈ 𝐶 )
124 onelon ⊢ ( ( 𝐶 ∈ On ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ On )
125 122 123 124 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑥 ∈ On )
126 121 125 46 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o 𝑥 ) ∈ On )
127 eloni ⊢ ( ( ω ↑o 𝑥 ) ∈ On → Ord ( ω ↑o 𝑥 ) )
128 126 127 syl ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → Ord ( ω ↑o 𝑥 ) )
129 simplrr ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝐴 ∈ ( ω ↑o 𝑥 ) )
130 ordelss ⊢ ( ( Ord ( ω ↑o 𝑥 ) ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) → 𝐴 ⊆ ( ω ↑o 𝑥 ) )
131 128 129 130 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝐴 ⊆ ( ω ↑o 𝑥 ) )
132 ssun1 ⊢ 𝑥 ⊆ ( 𝑥 ∪ 𝑧 )
133 26 ad3antrrr ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → Ord 𝐶 )
134 simprl ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑧 ∈ 𝐶 )
135 ordunel ⊢ ( ( Ord 𝐶 ∧ 𝑥 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑥 ∪ 𝑧 ) ∈ 𝐶 )
136 133 123 134 135 syl3anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝑥 ∪ 𝑧 ) ∈ 𝐶 )
137 onelon ⊢ ( ( 𝐶 ∈ On ∧ ( 𝑥 ∪ 𝑧 ) ∈ 𝐶 ) → ( 𝑥 ∪ 𝑧 ) ∈ On )
138 122 136 137 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝑥 ∪ 𝑧 ) ∈ On )
139 peano1 ⊢ ∅ ∈ ω
140 139 a1i ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ∅ ∈ ω )
141 oewordi ⊢ ( ( ( 𝑥 ∈ On ∧ ( 𝑥 ∪ 𝑧 ) ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) → ( 𝑥 ⊆ ( 𝑥 ∪ 𝑧 ) → ( ω ↑o 𝑥 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
142 125 138 121 140 141 syl31anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝑥 ⊆ ( 𝑥 ∪ 𝑧 ) → ( ω ↑o 𝑥 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
143 132 142 mpi ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o 𝑥 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) )
144 131 143 sstrd ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝐴 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) )
145 102 adantr ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝐴 ∈ On )
146 oecl ⊢ ( ( ω ∈ On ∧ ( 𝑥 ∪ 𝑧 ) ∈ On ) → ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On )
147 121 138 146 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On )
148 onelon ⊢ ( ( 𝐶 ∈ On ∧ 𝑧 ∈ 𝐶 ) → 𝑧 ∈ On )
149 122 134 148 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑧 ∈ On )
150 oecl ⊢ ( ( ω ∈ On ∧ 𝑧 ∈ On ) → ( ω ↑o 𝑧 ) ∈ On )
151 121 149 150 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o 𝑧 ) ∈ On )
152 simprr ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑦 ∈ ( ω ↑o 𝑧 ) )
153 onelon ⊢ ( ( ( ω ↑o 𝑧 ) ∈ On ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) → 𝑦 ∈ On )
154 151 152 153 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑦 ∈ On )
155 oawordri ⊢ ( ( 𝐴 ∈ On ∧ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) ) )
156 145 147 154 155 syl3anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝐴 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) ) )
157 144 156 mpd ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) )
158 eloni ⊢ ( ( ω ↑o 𝑧 ) ∈ On → Ord ( ω ↑o 𝑧 ) )
159 151 158 syl ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → Ord ( ω ↑o 𝑧 ) )
160 ordelss ⊢ ( ( Ord ( ω ↑o 𝑧 ) ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) → 𝑦 ⊆ ( ω ↑o 𝑧 ) )
161 159 152 160 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑦 ⊆ ( ω ↑o 𝑧 ) )
162 ssun2 ⊢ 𝑧 ⊆ ( 𝑥 ∪ 𝑧 )
163 oewordi ⊢ ( ( ( 𝑧 ∈ On ∧ ( 𝑥 ∪ 𝑧 ) ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) → ( 𝑧 ⊆ ( 𝑥 ∪ 𝑧 ) → ( ω ↑o 𝑧 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
164 149 138 121 140 163 syl31anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝑧 ⊆ ( 𝑥 ∪ 𝑧 ) → ( ω ↑o 𝑧 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
165 162 164 mpi ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o 𝑧 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) )
166 161 165 sstrd ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑦 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) )
167 oaword ⊢ ( ( 𝑦 ∈ On ∧ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On ∧ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On ) → ( 𝑦 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ↔ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ) )
168 154 147 147 167 syl3anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝑦 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ↔ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ) )
169 166 168 mpbid ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
170 157 169 sstrd ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
171 ordom ⊢ Ord ω
172 ordsucss ⊢ ( Ord ω → ( 1o ∈ ω → suc 1o ⊆ ω ) )
173 171 105 172 mp2 ⊢ suc 1o ⊆ ω
174 1on ⊢ 1o ∈ On
175 onsuc ⊢ ( 1o ∈ On → suc 1o ∈ On )
176 174 175 mp1i ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → suc 1o ∈ On )
177 omwordi ⊢ ( ( suc 1o ∈ On ∧ ω ∈ On ∧ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On ) → ( suc 1o ⊆ ω → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o ω ) ) )
178 176 121 147 177 syl3anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( suc 1o ⊆ ω → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o ω ) ) )
179 173 178 mpi ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o ω ) )
180 174 a1i ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 1o ∈ On )
181 omsuc ⊢ ( ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On ∧ 1o ∈ On ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) = ( ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o 1o ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
182 147 180 181 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) = ( ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o 1o ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
183 om1 ⊢ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o 1o ) = ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) )
184 147 183 syl ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o 1o ) = ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) )
185 184 oveq1d ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o 1o ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) = ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
186 182 185 eqtr2d ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) = ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) )
187 oesuc ⊢ ( ( ω ∈ On ∧ ( 𝑥 ∪ 𝑧 ) ∈ On ) → ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) = ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o ω ) )
188 121 138 187 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) = ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o ω ) )
189 179 186 188 3sstr4d ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ⊆ ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) )
190 170 189 sstrd ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) )
191 ordsucss ⊢ ( Ord 𝐶 → ( ( 𝑥 ∪ 𝑧 ) ∈ 𝐶 → suc ( 𝑥 ∪ 𝑧 ) ⊆ 𝐶 ) )
192 133 136 191 sylc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → suc ( 𝑥 ∪ 𝑧 ) ⊆ 𝐶 )
193 onsuc ⊢ ( ( 𝑥 ∪ 𝑧 ) ∈ On → suc ( 𝑥 ∪ 𝑧 ) ∈ On )
194 138 193 syl ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → suc ( 𝑥 ∪ 𝑧 ) ∈ On )
195 oewordi ⊢ ( ( ( suc ( 𝑥 ∪ 𝑧 ) ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) → ( suc ( 𝑥 ∪ 𝑧 ) ⊆ 𝐶 → ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) ⊆ ( ω ↑o 𝐶 ) ) )
196 194 122 121 140 195 syl31anc ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( suc ( 𝑥 ∪ 𝑧 ) ⊆ 𝐶 → ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) ⊆ ( ω ↑o 𝐶 ) ) )
197 192 196 mpd ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) ⊆ ( ω ↑o 𝐶 ) )
198 190 197 sstrd ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) )
199 198 expr ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 ∈ ( ω ↑o 𝑧 ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ) )
200 120 199 sylan2 ⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ 𝑧 ∈ ( 𝐶 ∖ 1o ) ) → ( 𝑦 ∈ ( ω ↑o 𝑧 ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ) )
201 200 rexlimdva ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( ∃ 𝑧 ∈ ( 𝐶 ∖ 1o ) 𝑦 ∈ ( ω ↑o 𝑧 ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ) )
202 119 201 sylbid ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( 𝑦 ∈ ( ω ↑o 𝐶 ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ) )
203 202 ralrimiv ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ∀ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) )
204 iunss ⊢ ( ∪ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ↔ ∀ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) )
205 203 204 sylibr ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ∪ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) )
206 113 205 eqsstrd ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) )
207 206 expr ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝐴 ∈ ( ω ↑o 𝑥 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) ) )
208 101 207 sylan2 ⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ 𝑥 ∈ ( 𝐶 ∖ 1o ) ) → ( 𝐴 ∈ ( ω ↑o 𝑥 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) ) )
209 208 rexlimdva ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( ∃ 𝑥 ∈ ( 𝐶 ∖ 1o ) 𝐴 ∈ ( ω ↑o 𝑥 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) ) )
210 100 209 mpd ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) )
211 88 adantr ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( ω ↑o 𝐶 ) ⊆ ( 𝐴 +o ( ω ↑o 𝐶 ) ) )
212 210 211 eqssd ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
213 212 ex ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( Lim 𝐶 → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) )
214 43 91 213 3jaod ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ( 𝐶 = ∅ ∨ ∃ 𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) )
215 28 214 mpd ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
216 215 adantr ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
217 216 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( ( 𝐴 +o ( ω ↑o 𝐶 ) ) +o 𝑥 ) = ( ( ω ↑o 𝐶 ) +o 𝑥 ) )
218 23 217 eqtr3d ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( 𝐴 +o ( ( ω ↑o 𝐶 ) +o 𝑥 ) ) = ( ( ω ↑o 𝐶 ) +o 𝑥 ) )
219 oveq2 ⊢ ( ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ( 𝐴 +o ( ( ω ↑o 𝐶 ) +o 𝑥 ) ) = ( 𝐴 +o 𝐵 ) )
220 id ⊢ ( ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 )
221 219 220 eqeq12d ⊢ ( ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ( ( 𝐴 +o ( ( ω ↑o 𝐶 ) +o 𝑥 ) ) = ( ( ω ↑o 𝐶 ) +o 𝑥 ) ↔ ( 𝐴 +o 𝐵 ) = 𝐵 ) )
222 218 221 syl5ibcom ⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ( 𝐴 +o 𝐵 ) = 𝐵 ) )
223 222 rexlimdva ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ∃ 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ( 𝐴 +o 𝐵 ) = 𝐵 ) )
224 15 223 mpd ⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( 𝐴 +o 𝐵 ) = 𝐵 )