Metamath Proof Explorer

Theorem omabs2

Description: Ordinal multiplication by a larger ordinal is absorbed when the larger ordinal is either 2 or _om raised to some power of _om . (Contributed by RP, 12-Jan-2025)

Ref Expression
Assertion omabs2 ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ∅ ∨ 𝐵 = 2o ∨ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ) → ( 𝐴 ·o 𝐵 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ ( 𝐵 = ∅ → ( 𝐴 ∈ 𝐵 ↔ 𝐴 ∈ ∅ ) )
2 noel ⊢ ¬ 𝐴 ∈ ∅
3 2 pm2.21i ⊢ ( 𝐴 ∈ ∅ → ( ∅ ∈ 𝐴 → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
4 1 3 biimtrdi ⊢ ( 𝐵 = ∅ → ( 𝐴 ∈ 𝐵 → ( ∅ ∈ 𝐴 → ( 𝐴 ·o 𝐵 ) = 𝐵 ) ) )
5 4 impd ⊢ ( 𝐵 = ∅ → ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
6 5 com12 ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) → ( 𝐵 = ∅ → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
7 elpri ⊢ ( 𝐴 ∈ { ∅ , 1o } → ( 𝐴 = ∅ ∨ 𝐴 = 1o ) )
8 eleq2 ⊢ ( 𝐴 = ∅ → ( ∅ ∈ 𝐴 ↔ ∅ ∈ ∅ ) )
9 noel ⊢ ¬ ∅ ∈ ∅
10 9 pm2.21i ⊢ ( ∅ ∈ ∅ → ( 𝐴 ·o 2o ) = 2o )
11 8 10 biimtrdi ⊢ ( 𝐴 = ∅ → ( ∅ ∈ 𝐴 → ( 𝐴 ·o 2o ) = 2o ) )
12 oveq1 ⊢ ( 𝐴 = 1o → ( 𝐴 ·o 2o ) = ( 1o ·o 2o ) )
13 2on ⊢ 2o ∈ On
14 om1r ⊢ ( 2o ∈ On → ( 1o ·o 2o ) = 2o )
15 13 14 ax-mp ⊢ ( 1o ·o 2o ) = 2o
16 12 15 eqtrdi ⊢ ( 𝐴 = 1o → ( 𝐴 ·o 2o ) = 2o )
17 16 a1d ⊢ ( 𝐴 = 1o → ( ∅ ∈ 𝐴 → ( 𝐴 ·o 2o ) = 2o ) )
18 11 17 jaoi ⊢ ( ( 𝐴 = ∅ ∨ 𝐴 = 1o ) → ( ∅ ∈ 𝐴 → ( 𝐴 ·o 2o ) = 2o ) )
19 7 18 syl ⊢ ( 𝐴 ∈ { ∅ , 1o } → ( ∅ ∈ 𝐴 → ( 𝐴 ·o 2o ) = 2o ) )
20 df2o3 ⊢ 2o = { ∅ , 1o }
21 19 20 eleq2s ⊢ ( 𝐴 ∈ 2o → ( ∅ ∈ 𝐴 → ( 𝐴 ·o 2o ) = 2o ) )
22 21 imp ⊢ ( ( 𝐴 ∈ 2o ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ·o 2o ) = 2o )
23 22 a1i ⊢ ( 𝐵 = 2o → ( ( 𝐴 ∈ 2o ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ·o 2o ) = 2o ) )
24 eleq2 ⊢ ( 𝐵 = 2o → ( 𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 2o ) )
25 24 anbi1d ⊢ ( 𝐵 = 2o → ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ↔ ( 𝐴 ∈ 2o ∧ ∅ ∈ 𝐴 ) ) )
26 oveq2 ⊢ ( 𝐵 = 2o → ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 2o ) )
27 id ⊢ ( 𝐵 = 2o → 𝐵 = 2o )
28 26 27 eqeq12d ⊢ ( 𝐵 = 2o → ( ( 𝐴 ·o 𝐵 ) = 𝐵 ↔ ( 𝐴 ·o 2o ) = 2o ) )
29 23 25 28 3imtr4d ⊢ ( 𝐵 = 2o → ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
30 29 com12 ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) → ( 𝐵 = 2o → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
31 simpr ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ 𝐴 ∈ ω ) → 𝐴 ∈ ω )
32 simpllr ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ 𝐴 ∈ ω ) → ∅ ∈ 𝐴 )
33 omelon ⊢ ω ∈ On
34 oecl ⊢ ( ( ω ∈ On ∧ 𝐶 ∈ On ) → ( ω ↑o 𝐶 ) ∈ On )
35 33 34 mpan ⊢ ( 𝐶 ∈ On → ( ω ↑o 𝐶 ) ∈ On )
36 35 adantl ⊢ ( ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) → ( ω ↑o 𝐶 ) ∈ On )
37 36 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ 𝐴 ∈ ω ) → ( ω ↑o 𝐶 ) ∈ On )
38 33 jctl ⊢ ( 𝐶 ∈ On → ( ω ∈ On ∧ 𝐶 ∈ On ) )
39 peano1 ⊢ ∅ ∈ ω
40 oen0 ⊢ ( ( ( ω ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ ω ) → ∅ ∈ ( ω ↑o 𝐶 ) )
41 38 39 40 sylancl ⊢ ( 𝐶 ∈ On → ∅ ∈ ( ω ↑o 𝐶 ) )
42 41 adantl ⊢ ( ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) → ∅ ∈ ( ω ↑o 𝐶 ) )
43 42 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ 𝐴 ∈ ω ) → ∅ ∈ ( ω ↑o 𝐶 ) )
44 omabs ⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ( ω ↑o 𝐶 ) ∈ On ∧ ∅ ∈ ( ω ↑o 𝐶 ) ) ) → ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
45 31 32 37 43 44 syl22anc ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ 𝐴 ∈ ω ) → ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
46 oveq2 ⊢ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) → ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
47 id ⊢ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) → 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) )
48 46 47 eqeq12d ⊢ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) → ( ( 𝐴 ·o 𝐵 ) = 𝐵 ↔ ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
49 48 adantr ⊢ ( ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) = 𝐵 ↔ ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
50 49 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ 𝐴 ∈ ω ) → ( ( 𝐴 ·o 𝐵 ) = 𝐵 ↔ ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
51 45 50 mpbird ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ 𝐴 ∈ ω ) → ( 𝐴 ·o 𝐵 ) = 𝐵 )
52 simpl ⊢ ( ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) → 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) )
53 oecl ⊢ ( ( ω ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ) → ( ω ↑o ( ω ↑o 𝐶 ) ) ∈ On )
54 33 35 53 sylancr ⊢ ( 𝐶 ∈ On → ( ω ↑o ( ω ↑o 𝐶 ) ) ∈ On )
55 54 adantl ⊢ ( ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) → ( ω ↑o ( ω ↑o 𝐶 ) ) ∈ On )
56 52 55 eqeltrd ⊢ ( ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) → 𝐵 ∈ On )
57 simpl ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) → 𝐴 ∈ 𝐵 )
58 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ On )
59 56 57 58 syl2anr ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) → 𝐴 ∈ On )
60 simplr ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) → ∅ ∈ 𝐴 )
61 ondif1 ⊢ ( 𝐴 ∈ ( On ∖ 1o ) ↔ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) )
62 59 60 61 sylanbrc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) → 𝐴 ∈ ( On ∖ 1o ) )
63 1onn ⊢ 1o ∈ ω
64 ondif2 ⊢ ( ω ∈ ( On ∖ 2o ) ↔ ( ω ∈ On ∧ 1o ∈ ω ) )
65 33 63 64 mpbir2an ⊢ ω ∈ ( On ∖ 2o )
66 62 65 jctil ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) → ( ω ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ ( On ∖ 1o ) ) )
67 66 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) → ( ω ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ ( On ∖ 1o ) ) )
68 oeeu ⊢ ( ( ω ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ ( On ∖ 1o ) ) → ∃! 𝑤 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( ω ∖ 1o ) ∃ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) )
69 67 68 syl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) → ∃! 𝑤 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( ω ∖ 1o ) ∃ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) )
70 euex ⊢ ( ∃! 𝑤 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( ω ∖ 1o ) ∃ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ∃ 𝑤 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( ω ∖ 1o ) ∃ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) )
71 simpr ⊢ ( ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 )
72 0ss ⊢ ∅ ⊆ 𝑧
73 0elon ⊢ ∅ ∈ On
74 simpr ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) → 𝑥 ∈ On )
75 oecl ⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ) → ( ω ↑o 𝑥 ) ∈ On )
76 33 74 75 sylancr ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) → ( ω ↑o 𝑥 ) ∈ On )
77 76 ad2antrr ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) → ( ω ↑o 𝑥 ) ∈ On )
78 onelon ⊢ ( ( ( ω ↑o 𝑥 ) ∈ On ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) → 𝑧 ∈ On )
79 77 78 sylancom ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) → 𝑧 ∈ On )
80 1on ⊢ 1o ∈ On
81 omcl ⊢ ( ( ( ω ↑o 𝑥 ) ∈ On ∧ 1o ∈ On ) → ( ( ω ↑o 𝑥 ) ·o 1o ) ∈ On )
82 76 80 81 sylancl ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) → ( ( ω ↑o 𝑥 ) ·o 1o ) ∈ On )
83 82 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ω ↑o 𝑥 ) ·o 1o ) ∈ On )
84 oaword ⊢ ( ( ∅ ∈ On ∧ 𝑧 ∈ On ∧ ( ( ω ↑o 𝑥 ) ·o 1o ) ∈ On ) → ( ∅ ⊆ 𝑧 ↔ ( ( ( ω ↑o 𝑥 ) ·o 1o ) +o ∅ ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 1o ) +o 𝑧 ) ) )
85 84 biimpd ⊢ ( ( ∅ ∈ On ∧ 𝑧 ∈ On ∧ ( ( ω ↑o 𝑥 ) ·o 1o ) ∈ On ) → ( ∅ ⊆ 𝑧 → ( ( ( ω ↑o 𝑥 ) ·o 1o ) +o ∅ ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 1o ) +o 𝑧 ) ) )
86 73 79 83 85 mp3an2ani ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ∅ ⊆ 𝑧 → ( ( ( ω ↑o 𝑥 ) ·o 1o ) +o ∅ ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 1o ) +o 𝑧 ) ) )
87 72 86 mpi ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ( ω ↑o 𝑥 ) ·o 1o ) +o ∅ ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 1o ) +o 𝑧 ) )
88 simpllr ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 𝑦 ∈ ( ω ∖ 1o ) )
89 omsson ⊢ ω ⊆ On
90 ssdif ⊢ ( ω ⊆ On → ( ω ∖ 1o ) ⊆ ( On ∖ 1o ) )
91 89 90 ax-mp ⊢ ( ω ∖ 1o ) ⊆ ( On ∖ 1o )
92 91 sseli ⊢ ( 𝑦 ∈ ( ω ∖ 1o ) → 𝑦 ∈ ( On ∖ 1o ) )
93 ondif1 ⊢ ( 𝑦 ∈ ( On ∖ 1o ) ↔ ( 𝑦 ∈ On ∧ ∅ ∈ 𝑦 ) )
94 df-1o ⊢ 1o = suc ∅
95 eloni ⊢ ( 𝑦 ∈ On → Ord 𝑦 )
96 ordsucss ⊢ ( Ord 𝑦 → ( ∅ ∈ 𝑦 → suc ∅ ⊆ 𝑦 ) )
97 95 96 syl ⊢ ( 𝑦 ∈ On → ( ∅ ∈ 𝑦 → suc ∅ ⊆ 𝑦 ) )
98 97 imp ⊢ ( ( 𝑦 ∈ On ∧ ∅ ∈ 𝑦 ) → suc ∅ ⊆ 𝑦 )
99 94 98 eqsstrid ⊢ ( ( 𝑦 ∈ On ∧ ∅ ∈ 𝑦 ) → 1o ⊆ 𝑦 )
100 93 99 sylbi ⊢ ( 𝑦 ∈ ( On ∖ 1o ) → 1o ⊆ 𝑦 )
101 88 92 100 3syl ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 1o ⊆ 𝑦 )
102 eldifi ⊢ ( 𝑦 ∈ ( ω ∖ 1o ) → 𝑦 ∈ ω )
103 nnon ⊢ ( 𝑦 ∈ ω → 𝑦 ∈ On )
104 102 103 syl ⊢ ( 𝑦 ∈ ( ω ∖ 1o ) → 𝑦 ∈ On )
105 104 ad2antlr ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) → 𝑦 ∈ On )
106 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 𝑥 ∈ On )
107 33 106 75 sylancr ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ω ↑o 𝑥 ) ∈ On )
108 omwordi ⊢ ( ( 1o ∈ On ∧ 𝑦 ∈ On ∧ ( ω ↑o 𝑥 ) ∈ On ) → ( 1o ⊆ 𝑦 → ( ( ω ↑o 𝑥 ) ·o 1o ) ⊆ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) )
109 80 105 107 108 mp3an2ani ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 1o ⊆ 𝑦 → ( ( ω ↑o 𝑥 ) ·o 1o ) ⊆ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) )
110 101 109 mpd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ω ↑o 𝑥 ) ·o 1o ) ⊆ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) )
111 105 adantr ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 𝑦 ∈ On )
112 omcl ⊢ ( ( ( ω ↑o 𝑥 ) ∈ On ∧ 𝑦 ∈ On ) → ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∈ On )
113 107 111 112 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∈ On )
114 79 adantr ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 𝑧 ∈ On )
115 oawordri ⊢ ( ( ( ( ω ↑o 𝑥 ) ·o 1o ) ∈ On ∧ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∈ On ∧ 𝑧 ∈ On ) → ( ( ( ω ↑o 𝑥 ) ·o 1o ) ⊆ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) → ( ( ( ω ↑o 𝑥 ) ·o 1o ) +o 𝑧 ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) ) )
116 83 113 114 115 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ( ω ↑o 𝑥 ) ·o 1o ) ⊆ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) → ( ( ( ω ↑o 𝑥 ) ·o 1o ) +o 𝑧 ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) ) )
117 110 116 mpd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ( ω ↑o 𝑥 ) ·o 1o ) +o 𝑧 ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) )
118 87 117 sstrd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ( ω ↑o 𝑥 ) ·o 1o ) +o ∅ ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) )
119 33 75 mpan ⊢ ( 𝑥 ∈ On → ( ω ↑o 𝑥 ) ∈ On )
120 119 80 81 sylancl ⊢ ( 𝑥 ∈ On → ( ( ω ↑o 𝑥 ) ·o 1o ) ∈ On )
121 oa0 ⊢ ( ( ( ω ↑o 𝑥 ) ·o 1o ) ∈ On → ( ( ( ω ↑o 𝑥 ) ·o 1o ) +o ∅ ) = ( ( ω ↑o 𝑥 ) ·o 1o ) )
122 120 121 syl ⊢ ( 𝑥 ∈ On → ( ( ( ω ↑o 𝑥 ) ·o 1o ) +o ∅ ) = ( ( ω ↑o 𝑥 ) ·o 1o ) )
123 om1 ⊢ ( ( ω ↑o 𝑥 ) ∈ On → ( ( ω ↑o 𝑥 ) ·o 1o ) = ( ω ↑o 𝑥 ) )
124 119 123 syl ⊢ ( 𝑥 ∈ On → ( ( ω ↑o 𝑥 ) ·o 1o ) = ( ω ↑o 𝑥 ) )
125 122 124 eqtrd ⊢ ( 𝑥 ∈ On → ( ( ( ω ↑o 𝑥 ) ·o 1o ) +o ∅ ) = ( ω ↑o 𝑥 ) )
126 106 125 syl ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ( ω ↑o 𝑥 ) ·o 1o ) +o ∅ ) = ( ω ↑o 𝑥 ) )
127 simpr ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 )
128 118 126 127 3sstr3d ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ω ↑o 𝑥 ) ⊆ 𝐴 )
129 simp-7l ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 𝐴 ∈ 𝐵 )
130 simplrl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) → 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) )
131 130 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) )
132 129 131 eleqtrd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 𝐴 ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) )
133 55 ad6antlr ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ω ↑o ( ω ↑o 𝐶 ) ) ∈ On )
134 ontr2 ⊢ ( ( ( ω ↑o 𝑥 ) ∈ On ∧ ( ω ↑o ( ω ↑o 𝐶 ) ) ∈ On ) → ( ( ( ω ↑o 𝑥 ) ⊆ 𝐴 ∧ 𝐴 ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) → ( ω ↑o 𝑥 ) ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
135 107 133 134 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ( ω ↑o 𝑥 ) ⊆ 𝐴 ∧ 𝐴 ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) → ( ω ↑o 𝑥 ) ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
136 128 132 135 mp2and ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ω ↑o 𝑥 ) ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) )
137 36 ad6antlr ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ω ↑o 𝐶 ) ∈ On )
138 65 a1i ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ω ∈ ( On ∖ 2o ) )
139 oeord ⊢ ( ( 𝑥 ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ∧ ω ∈ ( On ∖ 2o ) ) → ( 𝑥 ∈ ( ω ↑o 𝐶 ) ↔ ( ω ↑o 𝑥 ) ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
140 106 137 138 139 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝑥 ∈ ( ω ↑o 𝐶 ) ↔ ( ω ↑o 𝑥 ) ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
141 136 140 mpbird ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 𝑥 ∈ ( ω ↑o 𝐶 ) )
142 simp-5r ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ω ⊆ 𝐴 )
143 142 128 unssd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 )
144 simplr ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 𝑧 ∈ ( ω ↑o 𝑥 ) )
145 onelpss ⊢ ( ( 𝑧 ∈ On ∧ ( ω ↑o 𝑥 ) ∈ On ) → ( 𝑧 ∈ ( ω ↑o 𝑥 ) ↔ ( 𝑧 ⊆ ( ω ↑o 𝑥 ) ∧ 𝑧 ≠ ( ω ↑o 𝑥 ) ) ) )
146 145 biimpd ⊢ ( ( 𝑧 ∈ On ∧ ( ω ↑o 𝑥 ) ∈ On ) → ( 𝑧 ∈ ( ω ↑o 𝑥 ) → ( 𝑧 ⊆ ( ω ↑o 𝑥 ) ∧ 𝑧 ≠ ( ω ↑o 𝑥 ) ) ) )
147 79 107 146 syl2an2r ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝑧 ∈ ( ω ↑o 𝑥 ) → ( 𝑧 ⊆ ( ω ↑o 𝑥 ) ∧ 𝑧 ≠ ( ω ↑o 𝑥 ) ) ) )
148 144 147 mpd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝑧 ⊆ ( ω ↑o 𝑥 ) ∧ 𝑧 ≠ ( ω ↑o 𝑥 ) ) )
149 simpl ⊢ ( ( 𝑧 ⊆ ( ω ↑o 𝑥 ) ∧ 𝑧 ≠ ( ω ↑o 𝑥 ) ) → 𝑧 ⊆ ( ω ↑o 𝑥 ) )
150 148 149 syl ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 𝑧 ⊆ ( ω ↑o 𝑥 ) )
151 oaword ⊢ ( ( 𝑧 ∈ On ∧ ( ω ↑o 𝑥 ) ∈ On ∧ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∈ On ) → ( 𝑧 ⊆ ( ω ↑o 𝑥 ) ↔ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝑥 ) ) ) )
152 151 biimpd ⊢ ( ( 𝑧 ∈ On ∧ ( ω ↑o 𝑥 ) ∈ On ∧ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∈ On ) → ( 𝑧 ⊆ ( ω ↑o 𝑥 ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝑥 ) ) ) )
153 114 107 113 152 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝑧 ⊆ ( ω ↑o 𝑥 ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝑥 ) ) ) )
154 150 153 mpd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝑥 ) ) )
155 omsuc ⊢ ( ( ( ω ↑o 𝑥 ) ∈ On ∧ 𝑦 ∈ On ) → ( ( ω ↑o 𝑥 ) ·o suc 𝑦 ) = ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝑥 ) ) )
156 107 111 155 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ω ↑o 𝑥 ) ·o suc 𝑦 ) = ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝑥 ) ) )
157 154 156 sseqtrrd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) ⊆ ( ( ω ↑o 𝑥 ) ·o suc 𝑦 ) )
158 ordom ⊢ Ord ω
159 88 102 syl ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 𝑦 ∈ ω )
160 ordsucss ⊢ ( Ord ω → ( 𝑦 ∈ ω → suc 𝑦 ⊆ ω ) )
161 158 159 160 mpsyl ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → suc 𝑦 ⊆ ω )
162 oe1 ⊢ ( ω ∈ On → ( ω ↑o 1o ) = ω )
163 33 162 ax-mp ⊢ ( ω ↑o 1o ) = ω
164 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) ∧ 𝑥 = ∅ ) → 𝑥 = ∅ )
165 164 oveq2d ⊢ ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) ∧ 𝑥 = ∅ ) → ( ω ↑o 𝑥 ) = ( ω ↑o ∅ ) )
166 oe0 ⊢ ( ω ∈ On → ( ω ↑o ∅ ) = 1o )
167 33 166 ax-mp ⊢ ( ω ↑o ∅ ) = 1o
168 165 167 eqtrdi ⊢ ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) ∧ 𝑥 = ∅ ) → ( ω ↑o 𝑥 ) = 1o )
169 168 oveq1d ⊢ ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) ∧ 𝑥 = ∅ ) → ( ( ω ↑o 𝑥 ) ·o 𝑦 ) = ( 1o ·o 𝑦 ) )
170 104 adantl ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) → 𝑦 ∈ On )
171 170 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) ∧ 𝑥 = ∅ ) → 𝑦 ∈ On )
172 om1r ⊢ ( 𝑦 ∈ On → ( 1o ·o 𝑦 ) = 𝑦 )
173 171 172 syl ⊢ ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) ∧ 𝑥 = ∅ ) → ( 1o ·o 𝑦 ) = 𝑦 )
174 169 173 eqtrd ⊢ ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) ∧ 𝑥 = ∅ ) → ( ( ω ↑o 𝑥 ) ·o 𝑦 ) = 𝑦 )
175 simpllr ⊢ ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) ∧ 𝑥 = ∅ ) → 𝑧 ∈ ( ω ↑o 𝑥 ) )
176 175 168 eleqtrd ⊢ ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) ∧ 𝑥 = ∅ ) → 𝑧 ∈ 1o )
177 el1o ⊢ ( 𝑧 ∈ 1o ↔ 𝑧 = ∅ )
178 176 177 sylib ⊢ ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) ∧ 𝑥 = ∅ ) → 𝑧 = ∅ )
179 174 178 oveq12d ⊢ ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) ∧ 𝑥 = ∅ ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = ( 𝑦 +o ∅ ) )
180 simplr ⊢ ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) ∧ 𝑥 = ∅ ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 )
181 oa0 ⊢ ( 𝑦 ∈ On → ( 𝑦 +o ∅ ) = 𝑦 )
182 171 181 syl ⊢ ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) ∧ 𝑥 = ∅ ) → ( 𝑦 +o ∅ ) = 𝑦 )
183 179 180 182 3eqtr3d ⊢ ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) ∧ 𝑥 = ∅ ) → 𝐴 = 𝑦 )
184 159 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) ∧ 𝑥 = ∅ ) → 𝑦 ∈ ω )
185 183 184 eqeltrd ⊢ ( ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) ∧ 𝑥 = ∅ ) → 𝐴 ∈ ω )
186 185 ex ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝑥 = ∅ → 𝐴 ∈ ω ) )
187 33 33 pm3.2i ⊢ ( ω ∈ On ∧ ω ∈ On )
188 ontr2 ⊢ ( ( ω ∈ On ∧ ω ∈ On ) → ( ( ω ⊆ 𝐴 ∧ 𝐴 ∈ ω ) → ω ∈ ω ) )
189 188 expd ⊢ ( ( ω ∈ On ∧ ω ∈ On ) → ( ω ⊆ 𝐴 → ( 𝐴 ∈ ω → ω ∈ ω ) ) )
190 187 142 189 mpsyl ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝐴 ∈ ω → ω ∈ ω ) )
191 elirr ⊢ ¬ ω ∈ ω
192 191 pm2.21i ⊢ ( ω ∈ ω → 1o ⊆ 𝑥 )
193 192 a1i ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ω ∈ ω → 1o ⊆ 𝑥 ) )
194 186 190 193 3syld ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝑥 = ∅ → 1o ⊆ 𝑥 ) )
195 eloni ⊢ ( 𝑥 ∈ On → Ord 𝑥 )
196 ordsucss ⊢ ( Ord 𝑥 → ( ∅ ∈ 𝑥 → suc ∅ ⊆ 𝑥 ) )
197 196 imp ⊢ ( ( Ord 𝑥 ∧ ∅ ∈ 𝑥 ) → suc ∅ ⊆ 𝑥 )
198 94 197 eqsstrid ⊢ ( ( Ord 𝑥 ∧ ∅ ∈ 𝑥 ) → 1o ⊆ 𝑥 )
199 198 ex ⊢ ( Ord 𝑥 → ( ∅ ∈ 𝑥 → 1o ⊆ 𝑥 ) )
200 106 195 199 3syl ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ∅ ∈ 𝑥 → 1o ⊆ 𝑥 ) )
201 on0eqel ⊢ ( 𝑥 ∈ On → ( 𝑥 = ∅ ∨ ∅ ∈ 𝑥 ) )
202 106 201 syl ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝑥 = ∅ ∨ ∅ ∈ 𝑥 ) )
203 194 200 202 mpjaod ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 1o ⊆ 𝑥 )
204 80 a1i ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 1o ∈ On )
205 33 a1i ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ω ∈ On )
206 204 106 205 3jca ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ On ) )
207 oewordi ⊢ ( ( ( 1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) → ( 1o ⊆ 𝑥 → ( ω ↑o 1o ) ⊆ ( ω ↑o 𝑥 ) ) )
208 206 39 207 sylancl ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 1o ⊆ 𝑥 → ( ω ↑o 1o ) ⊆ ( ω ↑o 𝑥 ) ) )
209 203 208 mpd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ω ↑o 1o ) ⊆ ( ω ↑o 𝑥 ) )
210 163 209 eqsstrrid ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ω ⊆ ( ω ↑o 𝑥 ) )
211 161 210 sstrd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → suc 𝑦 ⊆ ( ω ↑o 𝑥 ) )
212 onsuc ⊢ ( 𝑦 ∈ On → suc 𝑦 ∈ On )
213 111 212 syl ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → suc 𝑦 ∈ On )
214 omwordi ⊢ ( ( suc 𝑦 ∈ On ∧ ( ω ↑o 𝑥 ) ∈ On ∧ ( ω ↑o 𝑥 ) ∈ On ) → ( suc 𝑦 ⊆ ( ω ↑o 𝑥 ) → ( ( ω ↑o 𝑥 ) ·o suc 𝑦 ) ⊆ ( ( ω ↑o 𝑥 ) ·o ( ω ↑o 𝑥 ) ) ) )
215 213 107 107 214 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( suc 𝑦 ⊆ ( ω ↑o 𝑥 ) → ( ( ω ↑o 𝑥 ) ·o suc 𝑦 ) ⊆ ( ( ω ↑o 𝑥 ) ·o ( ω ↑o 𝑥 ) ) ) )
216 211 215 mpd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ω ↑o 𝑥 ) ·o suc 𝑦 ) ⊆ ( ( ω ↑o 𝑥 ) ·o ( ω ↑o 𝑥 ) ) )
217 157 216 sstrd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) ⊆ ( ( ω ↑o 𝑥 ) ·o ( ω ↑o 𝑥 ) ) )
218 127 eqcomd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 𝐴 = ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) )
219 oeoa ⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ∧ 𝑥 ∈ On ) → ( ω ↑o ( 𝑥 +o 𝑥 ) ) = ( ( ω ↑o 𝑥 ) ·o ( ω ↑o 𝑥 ) ) )
220 33 106 106 219 mp3an2i ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ω ↑o ( 𝑥 +o 𝑥 ) ) = ( ( ω ↑o 𝑥 ) ·o ( ω ↑o 𝑥 ) ) )
221 217 218 220 3sstr4d ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) )
222 simpr3 ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) )
223 59 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → 𝐴 ∈ On )
224 simprr ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) → 𝐶 ∈ On )
225 simp1 ⊢ ( ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) → 𝑥 ∈ ( ω ↑o 𝐶 ) )
226 224 225 anim12i ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝐶 ∈ On ∧ 𝑥 ∈ ( ω ↑o 𝐶 ) ) )
227 onelon ⊢ ( ( ( ω ↑o 𝐶 ) ∈ On ∧ 𝑥 ∈ ( ω ↑o 𝐶 ) ) → 𝑥 ∈ On )
228 35 227 sylan ⊢ ( ( 𝐶 ∈ On ∧ 𝑥 ∈ ( ω ↑o 𝐶 ) ) → 𝑥 ∈ On )
229 pm4.24 ⊢ ( 𝑥 ∈ On ↔ ( 𝑥 ∈ On ∧ 𝑥 ∈ On ) )
230 228 229 sylib ⊢ ( ( 𝐶 ∈ On ∧ 𝑥 ∈ ( ω ↑o 𝐶 ) ) → ( 𝑥 ∈ On ∧ 𝑥 ∈ On ) )
231 oacl ⊢ ( ( 𝑥 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑥 +o 𝑥 ) ∈ On )
232 230 231 syl ⊢ ( ( 𝐶 ∈ On ∧ 𝑥 ∈ ( ω ↑o 𝐶 ) ) → ( 𝑥 +o 𝑥 ) ∈ On )
233 oecl ⊢ ( ( ω ∈ On ∧ ( 𝑥 +o 𝑥 ) ∈ On ) → ( ω ↑o ( 𝑥 +o 𝑥 ) ) ∈ On )
234 33 232 233 sylancr ⊢ ( ( 𝐶 ∈ On ∧ 𝑥 ∈ ( ω ↑o 𝐶 ) ) → ( ω ↑o ( 𝑥 +o 𝑥 ) ) ∈ On )
235 226 234 syl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ↑o ( 𝑥 +o 𝑥 ) ) ∈ On )
236 55 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ↑o ( ω ↑o 𝐶 ) ) ∈ On )
237 omwordri ⊢ ( ( 𝐴 ∈ On ∧ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ∈ On ∧ ( ω ↑o ( ω ↑o 𝐶 ) ) ∈ On ) → ( 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) → ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ⊆ ( ( ω ↑o ( 𝑥 +o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ) )
238 223 235 236 237 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) → ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ⊆ ( ( ω ↑o ( 𝑥 +o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ) )
239 222 238 mpd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ⊆ ( ( ω ↑o ( 𝑥 +o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
240 226 230 231 3syl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝑥 +o 𝑥 ) ∈ On )
241 36 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ↑o 𝐶 ) ∈ On )
242 oeoa ⊢ ( ( ω ∈ On ∧ ( 𝑥 +o 𝑥 ) ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ) → ( ω ↑o ( ( 𝑥 +o 𝑥 ) +o ( ω ↑o 𝐶 ) ) ) = ( ( ω ↑o ( 𝑥 +o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
243 33 240 241 242 mp3an2i ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ↑o ( ( 𝑥 +o 𝑥 ) +o ( ω ↑o 𝐶 ) ) ) = ( ( ω ↑o ( 𝑥 +o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
244 226 228 syl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → 𝑥 ∈ On )
245 oaass ⊢ ( ( 𝑥 ∈ On ∧ 𝑥 ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ) → ( ( 𝑥 +o 𝑥 ) +o ( ω ↑o 𝐶 ) ) = ( 𝑥 +o ( 𝑥 +o ( ω ↑o 𝐶 ) ) ) )
246 244 244 241 245 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ( 𝑥 +o 𝑥 ) +o ( ω ↑o 𝐶 ) ) = ( 𝑥 +o ( 𝑥 +o ( ω ↑o 𝐶 ) ) ) )
247 simpr1 ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → 𝑥 ∈ ( ω ↑o 𝐶 ) )
248 ssidd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ↑o 𝐶 ) ⊆ ( ω ↑o 𝐶 ) )
249 oaabs2 ⊢ ( ( ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ↑o 𝐶 ) ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ ( ω ↑o 𝐶 ) ) → ( 𝑥 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
250 247 241 248 249 syl21anc ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝑥 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
251 250 oveq2d ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝑥 +o ( 𝑥 +o ( ω ↑o 𝐶 ) ) ) = ( 𝑥 +o ( ω ↑o 𝐶 ) ) )
252 246 251 250 3eqtrd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ( 𝑥 +o 𝑥 ) +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
253 252 oveq2d ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ↑o ( ( 𝑥 +o 𝑥 ) +o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
254 243 253 eqtr3d ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ( ω ↑o ( 𝑥 +o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
255 239 254 sseqtrd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ⊆ ( ω ↑o ( ω ↑o 𝐶 ) ) )
256 oveq2 ⊢ ( 𝑥 = ∅ → ( ω ↑o 𝑥 ) = ( ω ↑o ∅ ) )
257 256 167 eqtrdi ⊢ ( 𝑥 = ∅ → ( ω ↑o 𝑥 ) = 1o )
258 257 uneq2d ⊢ ( 𝑥 = ∅ → ( ω ∪ ( ω ↑o 𝑥 ) ) = ( ω ∪ 1o ) )
259 33 oneluni ⊢ ( 1o ∈ ω → ( ω ∪ 1o ) = ω )
260 63 259 ax-mp ⊢ ( ω ∪ 1o ) = ω
261 260 163 eqtr4i ⊢ ( ω ∪ 1o ) = ( ω ↑o 1o )
262 258 261 eqtrdi ⊢ ( 𝑥 = ∅ → ( ω ∪ ( ω ↑o 𝑥 ) ) = ( ω ↑o 1o ) )
263 262 adantl ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( ω ∪ ( ω ↑o 𝑥 ) ) = ( ω ↑o 1o ) )
264 263 oveq1d ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ( ω ↑o 1o ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
265 224 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → 𝐶 ∈ On )
266 oecl ⊢ ( ( ω ∈ On ∧ ∅ ∈ On ) → ( ω ↑o ∅ ) ∈ On )
267 33 73 266 mp2an ⊢ ( ω ↑o ∅ ) ∈ On
268 oecl ⊢ ( ( ω ∈ On ∧ ( ω ↑o ∅ ) ∈ On ) → ( ω ↑o ( ω ↑o ∅ ) ) ∈ On )
269 33 267 268 mp2an ⊢ ( ω ↑o ( ω ↑o ∅ ) ) ∈ On
270 269 2a1i ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( 𝐶 ∈ On → ( ω ↑o ( ω ↑o ∅ ) ) ∈ On ) )
271 270 54 jca2 ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( 𝐶 ∈ On → ( ( ω ↑o ( ω ↑o ∅ ) ) ∈ On ∧ ( ω ↑o ( ω ↑o 𝐶 ) ) ∈ On ) ) )
272 167 oveq2i ⊢ ( ω ↑o ( ω ↑o ∅ ) ) = ( ω ↑o 1o )
273 272 163 eqtri ⊢ ( ω ↑o ( ω ↑o ∅ ) ) = ω
274 ssun1 ⊢ ω ⊆ ( ω ∪ ( ω ↑o 𝑥 ) )
275 273 274 eqsstri ⊢ ( ω ↑o ( ω ↑o ∅ ) ) ⊆ ( ω ∪ ( ω ↑o 𝑥 ) )
276 simp2 ⊢ ( ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) → ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 )
277 275 276 sstrid ⊢ ( ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) → ( ω ↑o ( ω ↑o ∅ ) ) ⊆ 𝐴 )
278 277 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ↑o ( ω ↑o ∅ ) ) ⊆ 𝐴 )
279 57 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → 𝐴 ∈ 𝐵 )
280 simplrl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) )
281 279 280 eleqtrd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → 𝐴 ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) )
282 278 281 jca ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ( ω ↑o ( ω ↑o ∅ ) ) ⊆ 𝐴 ∧ 𝐴 ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
283 282 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( ( ω ↑o ( ω ↑o ∅ ) ) ⊆ 𝐴 ∧ 𝐴 ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
284 ontr2 ⊢ ( ( ( ω ↑o ( ω ↑o ∅ ) ) ∈ On ∧ ( ω ↑o ( ω ↑o 𝐶 ) ) ∈ On ) → ( ( ( ω ↑o ( ω ↑o ∅ ) ) ⊆ 𝐴 ∧ 𝐴 ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) → ( ω ↑o ( ω ↑o ∅ ) ) ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
285 271 283 284 syl6ci ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( 𝐶 ∈ On → ( ω ↑o ( ω ↑o ∅ ) ) ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
286 oeord ⊢ ( ( ∅ ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ ( On ∖ 2o ) ) → ( ∅ ∈ 𝐶 ↔ ( ω ↑o ∅ ) ∈ ( ω ↑o 𝐶 ) ) )
287 73 65 286 mp3an13 ⊢ ( 𝐶 ∈ On → ( ∅ ∈ 𝐶 ↔ ( ω ↑o ∅ ) ∈ ( ω ↑o 𝐶 ) ) )
288 65 a1i ⊢ ( 𝐶 ∈ On → ω ∈ ( On ∖ 2o ) )
289 oeord ⊢ ( ( ( ω ↑o ∅ ) ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ∧ ω ∈ ( On ∖ 2o ) ) → ( ( ω ↑o ∅ ) ∈ ( ω ↑o 𝐶 ) ↔ ( ω ↑o ( ω ↑o ∅ ) ) ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
290 267 35 288 289 mp3an2i ⊢ ( 𝐶 ∈ On → ( ( ω ↑o ∅ ) ∈ ( ω ↑o 𝐶 ) ↔ ( ω ↑o ( ω ↑o ∅ ) ) ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
291 287 290 bitrd ⊢ ( 𝐶 ∈ On → ( ∅ ∈ 𝐶 ↔ ( ω ↑o ( ω ↑o ∅ ) ) ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
292 291 biimprd ⊢ ( 𝐶 ∈ On → ( ( ω ↑o ( ω ↑o ∅ ) ) ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) → ∅ ∈ 𝐶 ) )
293 285 292 sylcom ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( 𝐶 ∈ On → ∅ ∈ 𝐶 ) )
294 eloni ⊢ ( 𝐶 ∈ On → Ord 𝐶 )
295 ordsucss ⊢ ( Ord 𝐶 → ( ∅ ∈ 𝐶 → suc ∅ ⊆ 𝐶 ) )
296 94 sseq1i ⊢ ( 1o ⊆ 𝐶 ↔ suc ∅ ⊆ 𝐶 )
297 295 296 imbitrrdi ⊢ ( Ord 𝐶 → ( ∅ ∈ 𝐶 → 1o ⊆ 𝐶 ) )
298 294 297 syl ⊢ ( 𝐶 ∈ On → ( ∅ ∈ 𝐶 → 1o ⊆ 𝐶 ) )
299 293 298 sylcom ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( 𝐶 ∈ On → 1o ⊆ 𝐶 ) )
300 265 299 jcai ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) )
301 33 a1i ⊢ ( 𝐶 ∈ On → ω ∈ On )
302 80 a1i ⊢ ( 𝐶 ∈ On → 1o ∈ On )
303 301 302 35 3jca ⊢ ( 𝐶 ∈ On → ( ω ∈ On ∧ 1o ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ) )
304 303 adantr ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → ( ω ∈ On ∧ 1o ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ) )
305 oeoa ⊢ ( ( ω ∈ On ∧ 1o ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ) → ( ω ↑o ( 1o +o ( ω ↑o 𝐶 ) ) ) = ( ( ω ↑o 1o ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
306 304 305 syl ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → ( ω ↑o ( 1o +o ( ω ↑o 𝐶 ) ) ) = ( ( ω ↑o 1o ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
307 63 a1i ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → 1o ∈ ω )
308 35 adantr ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → ( ω ↑o 𝐶 ) ∈ On )
309 oeword ⊢ ( ( 1o ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ ( On ∖ 2o ) ) → ( 1o ⊆ 𝐶 ↔ ( ω ↑o 1o ) ⊆ ( ω ↑o 𝐶 ) ) )
310 80 65 309 mp3an13 ⊢ ( 𝐶 ∈ On → ( 1o ⊆ 𝐶 ↔ ( ω ↑o 1o ) ⊆ ( ω ↑o 𝐶 ) ) )
311 310 biimpa ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → ( ω ↑o 1o ) ⊆ ( ω ↑o 𝐶 ) )
312 163 311 eqsstrrid ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → ω ⊆ ( ω ↑o 𝐶 ) )
313 oaabs ⊢ ( ( ( 1o ∈ ω ∧ ( ω ↑o 𝐶 ) ∈ On ) ∧ ω ⊆ ( ω ↑o 𝐶 ) ) → ( 1o +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
314 307 308 312 313 syl21anc ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → ( 1o +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
315 314 oveq2d ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → ( ω ↑o ( 1o +o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
316 306 315 eqtr3d ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → ( ( ω ↑o 1o ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
317 300 316 syl ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( ( ω ↑o 1o ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
318 264 317 eqtrd ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
319 244 195 196 3syl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ∅ ∈ 𝑥 → suc ∅ ⊆ 𝑥 ) )
320 319 imp ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → suc ∅ ⊆ 𝑥 )
321 94 320 eqsstrid ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → 1o ⊆ 𝑥 )
322 247 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → 𝑥 ∈ ( ω ↑o 𝐶 ) )
323 241 322 227 syl2an2r ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → 𝑥 ∈ On )
324 65 a1i ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ω ∈ ( On ∖ 2o ) )
325 oeword ⊢ ( ( 1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ ( On ∖ 2o ) ) → ( 1o ⊆ 𝑥 ↔ ( ω ↑o 1o ) ⊆ ( ω ↑o 𝑥 ) ) )
326 80 323 324 325 mp3an2i ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( 1o ⊆ 𝑥 ↔ ( ω ↑o 1o ) ⊆ ( ω ↑o 𝑥 ) ) )
327 321 326 mpbid ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( ω ↑o 1o ) ⊆ ( ω ↑o 𝑥 ) )
328 163 327 eqsstrrid ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ω ⊆ ( ω ↑o 𝑥 ) )
329 ssequn1 ⊢ ( ω ⊆ ( ω ↑o 𝑥 ) ↔ ( ω ∪ ( ω ↑o 𝑥 ) ) = ( ω ↑o 𝑥 ) )
330 328 329 sylib ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( ω ∪ ( ω ↑o 𝑥 ) ) = ( ω ↑o 𝑥 ) )
331 330 oveq1d ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ( ω ↑o 𝑥 ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
332 241 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( ω ↑o 𝐶 ) ∈ On )
333 oeoa ⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ) → ( ω ↑o ( 𝑥 +o ( ω ↑o 𝐶 ) ) ) = ( ( ω ↑o 𝑥 ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
334 33 323 332 333 mp3an2i ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( ω ↑o ( 𝑥 +o ( ω ↑o 𝐶 ) ) ) = ( ( ω ↑o 𝑥 ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
335 ssidd ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( ω ↑o 𝐶 ) ⊆ ( ω ↑o 𝐶 ) )
336 322 332 335 249 syl21anc ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( 𝑥 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
337 336 oveq2d ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( ω ↑o ( 𝑥 +o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
338 331 334 337 3eqtr2d ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
339 226 228 201 3syl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝑥 = ∅ ∨ ∅ ∈ 𝑥 ) )
340 318 338 339 mpjaodan ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
341 276 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 )
342 33 228 75 sylancr ⊢ ( ( 𝐶 ∈ On ∧ 𝑥 ∈ ( ω ↑o 𝐶 ) ) → ( ω ↑o 𝑥 ) ∈ On )
343 342 33 jctil ⊢ ( ( 𝐶 ∈ On ∧ 𝑥 ∈ ( ω ↑o 𝐶 ) ) → ( ω ∈ On ∧ ( ω ↑o 𝑥 ) ∈ On ) )
344 onun2 ⊢ ( ( ω ∈ On ∧ ( ω ↑o 𝑥 ) ∈ On ) → ( ω ∪ ( ω ↑o 𝑥 ) ) ∈ On )
345 226 343 344 3syl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ∪ ( ω ↑o 𝑥 ) ) ∈ On )
346 omwordri ⊢ ( ( ( ω ∪ ( ω ↑o 𝑥 ) ) ∈ On ∧ 𝐴 ∈ On ∧ ( ω ↑o ( ω ↑o 𝐶 ) ) ∈ On ) → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ⊆ ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ) )
347 345 223 236 346 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ⊆ ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ) )
348 341 347 mpd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ⊆ ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
349 340 348 eqsstrrd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ↑o ( ω ↑o 𝐶 ) ) ⊆ ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
350 255 349 eqssd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
351 49 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ( 𝐴 ·o 𝐵 ) = 𝐵 ↔ ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
352 350 351 mpbird ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝐴 ·o 𝐵 ) = 𝐵 )
353 352 ex ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) → ( ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
354 353 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
355 141 143 221 354 mp3and ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝐴 ·o 𝐵 ) = 𝐵 )
356 355 ex ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) → ( ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
357 71 356 syl5 ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) → ( ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
358 357 rexlimdva ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) → ( ∃ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
359 358 rexlimdva ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) → ( ∃ 𝑦 ∈ ( ω ∖ 1o ) ∃ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
360 359 rexlimdva ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( ω ∖ 1o ) ∃ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
361 360 exlimdv ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) → ( ∃ 𝑤 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( ω ∖ 1o ) ∃ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
362 70 361 syl5 ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) → ( ∃! 𝑤 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( ω ∖ 1o ) ∃ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
363 69 362 mpd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) → ( 𝐴 ·o 𝐵 ) = 𝐵 )
364 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
365 59 364 syl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) → Ord 𝐴 )
366 ordtri2or ⊢ ( ( Ord 𝐴 ∧ Ord ω ) → ( 𝐴 ∈ ω ∨ ω ⊆ 𝐴 ) )
367 365 158 366 sylancl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) → ( 𝐴 ∈ ω ∨ ω ⊆ 𝐴 ) )
368 51 363 367 mpjaodan ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) → ( 𝐴 ·o 𝐵 ) = 𝐵 )
369 368 ex ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) → ( ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
370 6 30 369 3jaod ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) → ( ( 𝐵 = ∅ ∨ 𝐵 = 2o ∨ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
371 370 imp ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ∅ ∨ 𝐵 = 2o ∨ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ) → ( 𝐴 ·o 𝐵 ) = 𝐵 )