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 ordirr ⊢ ( Ord ω → ¬ ω ∈ ω )
192 158 191 ax-mp ⊢ ¬ ω ∈ ω
193 192 pm2.21i ⊢ ( ω ∈ ω → 1o ⊆ 𝑥 )
194 193 a1i ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ω ∈ ω → 1o ⊆ 𝑥 ) )
195 186 190 194 3syld ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝑥 = ∅ → 1o ⊆ 𝑥 ) )
196 eloni ⊢ ( 𝑥 ∈ On → Ord 𝑥 )
197 ordsucss ⊢ ( Ord 𝑥 → ( ∅ ∈ 𝑥 → suc ∅ ⊆ 𝑥 ) )
198 197 imp ⊢ ( ( Ord 𝑥 ∧ ∅ ∈ 𝑥 ) → suc ∅ ⊆ 𝑥 )
199 94 198 eqsstrid ⊢ ( ( Ord 𝑥 ∧ ∅ ∈ 𝑥 ) → 1o ⊆ 𝑥 )
200 199 ex ⊢ ( Ord 𝑥 → ( ∅ ∈ 𝑥 → 1o ⊆ 𝑥 ) )
201 106 196 200 3syl ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ∅ ∈ 𝑥 → 1o ⊆ 𝑥 ) )
202 on0eqel ⊢ ( 𝑥 ∈ On → ( 𝑥 = ∅ ∨ ∅ ∈ 𝑥 ) )
203 106 202 syl ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝑥 = ∅ ∨ ∅ ∈ 𝑥 ) )
204 195 201 203 mpjaod ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 1o ⊆ 𝑥 )
205 80 a1i ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 1o ∈ On )
206 33 a1i ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ω ∈ On )
207 205 106 206 3jca ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ On ) )
208 oewordi ⊢ ( ( ( 1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) → ( 1o ⊆ 𝑥 → ( ω ↑o 1o ) ⊆ ( ω ↑o 𝑥 ) ) )
209 207 39 208 sylancl ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 1o ⊆ 𝑥 → ( ω ↑o 1o ) ⊆ ( ω ↑o 𝑥 ) ) )
210 204 209 mpd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ω ↑o 1o ) ⊆ ( ω ↑o 𝑥 ) )
211 163 210 eqsstrrid ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ω ⊆ ( ω ↑o 𝑥 ) )
212 161 211 sstrd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → suc 𝑦 ⊆ ( ω ↑o 𝑥 ) )
213 onsuc ⊢ ( 𝑦 ∈ On → suc 𝑦 ∈ On )
214 111 213 syl ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → suc 𝑦 ∈ On )
215 omwordi ⊢ ( ( suc 𝑦 ∈ On ∧ ( ω ↑o 𝑥 ) ∈ On ∧ ( ω ↑o 𝑥 ) ∈ On ) → ( suc 𝑦 ⊆ ( ω ↑o 𝑥 ) → ( ( ω ↑o 𝑥 ) ·o suc 𝑦 ) ⊆ ( ( ω ↑o 𝑥 ) ·o ( ω ↑o 𝑥 ) ) ) )
216 214 107 107 215 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( suc 𝑦 ⊆ ( ω ↑o 𝑥 ) → ( ( ω ↑o 𝑥 ) ·o suc 𝑦 ) ⊆ ( ( ω ↑o 𝑥 ) ·o ( ω ↑o 𝑥 ) ) ) )
217 212 216 mpd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ω ↑o 𝑥 ) ·o suc 𝑦 ) ⊆ ( ( ω ↑o 𝑥 ) ·o ( ω ↑o 𝑥 ) ) )
218 157 217 sstrd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) ⊆ ( ( ω ↑o 𝑥 ) ·o ( ω ↑o 𝑥 ) ) )
219 127 eqcomd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 𝐴 = ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) )
220 oeoa ⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ∧ 𝑥 ∈ On ) → ( ω ↑o ( 𝑥 +o 𝑥 ) ) = ( ( ω ↑o 𝑥 ) ·o ( ω ↑o 𝑥 ) ) )
221 33 106 106 220 mp3an2i ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ω ↑o ( 𝑥 +o 𝑥 ) ) = ( ( ω ↑o 𝑥 ) ·o ( ω ↑o 𝑥 ) ) )
222 218 219 221 3sstr4d ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) )
223 simpr3 ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) )
224 59 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → 𝐴 ∈ On )
225 simprr ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) → 𝐶 ∈ On )
226 simp1 ⊢ ( ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) → 𝑥 ∈ ( ω ↑o 𝐶 ) )
227 225 226 anim12i ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝐶 ∈ On ∧ 𝑥 ∈ ( ω ↑o 𝐶 ) ) )
228 onelon ⊢ ( ( ( ω ↑o 𝐶 ) ∈ On ∧ 𝑥 ∈ ( ω ↑o 𝐶 ) ) → 𝑥 ∈ On )
229 35 228 sylan ⊢ ( ( 𝐶 ∈ On ∧ 𝑥 ∈ ( ω ↑o 𝐶 ) ) → 𝑥 ∈ On )
230 pm4.24 ⊢ ( 𝑥 ∈ On ↔ ( 𝑥 ∈ On ∧ 𝑥 ∈ On ) )
231 229 230 sylib ⊢ ( ( 𝐶 ∈ On ∧ 𝑥 ∈ ( ω ↑o 𝐶 ) ) → ( 𝑥 ∈ On ∧ 𝑥 ∈ On ) )
232 oacl ⊢ ( ( 𝑥 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑥 +o 𝑥 ) ∈ On )
233 231 232 syl ⊢ ( ( 𝐶 ∈ On ∧ 𝑥 ∈ ( ω ↑o 𝐶 ) ) → ( 𝑥 +o 𝑥 ) ∈ On )
234 oecl ⊢ ( ( ω ∈ On ∧ ( 𝑥 +o 𝑥 ) ∈ On ) → ( ω ↑o ( 𝑥 +o 𝑥 ) ) ∈ On )
235 33 233 234 sylancr ⊢ ( ( 𝐶 ∈ On ∧ 𝑥 ∈ ( ω ↑o 𝐶 ) ) → ( ω ↑o ( 𝑥 +o 𝑥 ) ) ∈ On )
236 227 235 syl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ↑o ( 𝑥 +o 𝑥 ) ) ∈ On )
237 55 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ↑o ( ω ↑o 𝐶 ) ) ∈ On )
238 omwordri ⊢ ( ( 𝐴 ∈ On ∧ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ∈ On ∧ ( ω ↑o ( ω ↑o 𝐶 ) ) ∈ On ) → ( 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) → ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ⊆ ( ( ω ↑o ( 𝑥 +o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ) )
239 224 236 237 238 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) → ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ⊆ ( ( ω ↑o ( 𝑥 +o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ) )
240 223 239 mpd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ⊆ ( ( ω ↑o ( 𝑥 +o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
241 227 231 232 3syl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝑥 +o 𝑥 ) ∈ On )
242 36 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ↑o 𝐶 ) ∈ On )
243 oeoa ⊢ ( ( ω ∈ On ∧ ( 𝑥 +o 𝑥 ) ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ) → ( ω ↑o ( ( 𝑥 +o 𝑥 ) +o ( ω ↑o 𝐶 ) ) ) = ( ( ω ↑o ( 𝑥 +o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
244 33 241 242 243 mp3an2i ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ↑o ( ( 𝑥 +o 𝑥 ) +o ( ω ↑o 𝐶 ) ) ) = ( ( ω ↑o ( 𝑥 +o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
245 227 229 syl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → 𝑥 ∈ On )
246 oaass ⊢ ( ( 𝑥 ∈ On ∧ 𝑥 ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ) → ( ( 𝑥 +o 𝑥 ) +o ( ω ↑o 𝐶 ) ) = ( 𝑥 +o ( 𝑥 +o ( ω ↑o 𝐶 ) ) ) )
247 245 245 242 246 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ( 𝑥 +o 𝑥 ) +o ( ω ↑o 𝐶 ) ) = ( 𝑥 +o ( 𝑥 +o ( ω ↑o 𝐶 ) ) ) )
248 simpr1 ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → 𝑥 ∈ ( ω ↑o 𝐶 ) )
249 ssidd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ↑o 𝐶 ) ⊆ ( ω ↑o 𝐶 ) )
250 oaabs2 ⊢ ( ( ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ↑o 𝐶 ) ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ ( ω ↑o 𝐶 ) ) → ( 𝑥 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
251 248 242 249 250 syl21anc ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝑥 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
252 251 oveq2d ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝑥 +o ( 𝑥 +o ( ω ↑o 𝐶 ) ) ) = ( 𝑥 +o ( ω ↑o 𝐶 ) ) )
253 247 252 251 3eqtrd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ( 𝑥 +o 𝑥 ) +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
254 253 oveq2d ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ↑o ( ( 𝑥 +o 𝑥 ) +o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
255 244 254 eqtr3d ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ( ω ↑o ( 𝑥 +o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
256 240 255 sseqtrd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ⊆ ( ω ↑o ( ω ↑o 𝐶 ) ) )
257 oveq2 ⊢ ( 𝑥 = ∅ → ( ω ↑o 𝑥 ) = ( ω ↑o ∅ ) )
258 257 167 eqtrdi ⊢ ( 𝑥 = ∅ → ( ω ↑o 𝑥 ) = 1o )
259 258 uneq2d ⊢ ( 𝑥 = ∅ → ( ω ∪ ( ω ↑o 𝑥 ) ) = ( ω ∪ 1o ) )
260 33 oneluni ⊢ ( 1o ∈ ω → ( ω ∪ 1o ) = ω )
261 63 260 ax-mp ⊢ ( ω ∪ 1o ) = ω
262 261 163 eqtr4i ⊢ ( ω ∪ 1o ) = ( ω ↑o 1o )
263 259 262 eqtrdi ⊢ ( 𝑥 = ∅ → ( ω ∪ ( ω ↑o 𝑥 ) ) = ( ω ↑o 1o ) )
264 263 adantl ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( ω ∪ ( ω ↑o 𝑥 ) ) = ( ω ↑o 1o ) )
265 264 oveq1d ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ( ω ↑o 1o ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
266 225 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → 𝐶 ∈ On )
267 oecl ⊢ ( ( ω ∈ On ∧ ∅ ∈ On ) → ( ω ↑o ∅ ) ∈ On )
268 33 73 267 mp2an ⊢ ( ω ↑o ∅ ) ∈ On
269 oecl ⊢ ( ( ω ∈ On ∧ ( ω ↑o ∅ ) ∈ On ) → ( ω ↑o ( ω ↑o ∅ ) ) ∈ On )
270 33 268 269 mp2an ⊢ ( ω ↑o ( ω ↑o ∅ ) ) ∈ On
271 270 2a1i ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( 𝐶 ∈ On → ( ω ↑o ( ω ↑o ∅ ) ) ∈ On ) )
272 271 54 jca2 ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( 𝐶 ∈ On → ( ( ω ↑o ( ω ↑o ∅ ) ) ∈ On ∧ ( ω ↑o ( ω ↑o 𝐶 ) ) ∈ On ) ) )
273 167 oveq2i ⊢ ( ω ↑o ( ω ↑o ∅ ) ) = ( ω ↑o 1o )
274 273 163 eqtri ⊢ ( ω ↑o ( ω ↑o ∅ ) ) = ω
275 ssun1 ⊢ ω ⊆ ( ω ∪ ( ω ↑o 𝑥 ) )
276 274 275 eqsstri ⊢ ( ω ↑o ( ω ↑o ∅ ) ) ⊆ ( ω ∪ ( ω ↑o 𝑥 ) )
277 simp2 ⊢ ( ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) → ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 )
278 276 277 sstrid ⊢ ( ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) → ( ω ↑o ( ω ↑o ∅ ) ) ⊆ 𝐴 )
279 278 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ↑o ( ω ↑o ∅ ) ) ⊆ 𝐴 )
280 57 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → 𝐴 ∈ 𝐵 )
281 simplrl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) )
282 280 281 eleqtrd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → 𝐴 ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) )
283 279 282 jca ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ( ω ↑o ( ω ↑o ∅ ) ) ⊆ 𝐴 ∧ 𝐴 ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
284 283 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( ( ω ↑o ( ω ↑o ∅ ) ) ⊆ 𝐴 ∧ 𝐴 ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
285 ontr2 ⊢ ( ( ( ω ↑o ( ω ↑o ∅ ) ) ∈ On ∧ ( ω ↑o ( ω ↑o 𝐶 ) ) ∈ On ) → ( ( ( ω ↑o ( ω ↑o ∅ ) ) ⊆ 𝐴 ∧ 𝐴 ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) → ( ω ↑o ( ω ↑o ∅ ) ) ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
286 272 284 285 syl6ci ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( 𝐶 ∈ On → ( ω ↑o ( ω ↑o ∅ ) ) ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
287 oeord ⊢ ( ( ∅ ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ ( On ∖ 2o ) ) → ( ∅ ∈ 𝐶 ↔ ( ω ↑o ∅ ) ∈ ( ω ↑o 𝐶 ) ) )
288 73 65 287 mp3an13 ⊢ ( 𝐶 ∈ On → ( ∅ ∈ 𝐶 ↔ ( ω ↑o ∅ ) ∈ ( ω ↑o 𝐶 ) ) )
289 65 a1i ⊢ ( 𝐶 ∈ On → ω ∈ ( On ∖ 2o ) )
290 oeord ⊢ ( ( ( ω ↑o ∅ ) ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ∧ ω ∈ ( On ∖ 2o ) ) → ( ( ω ↑o ∅ ) ∈ ( ω ↑o 𝐶 ) ↔ ( ω ↑o ( ω ↑o ∅ ) ) ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
291 268 35 289 290 mp3an2i ⊢ ( 𝐶 ∈ On → ( ( ω ↑o ∅ ) ∈ ( ω ↑o 𝐶 ) ↔ ( ω ↑o ( ω ↑o ∅ ) ) ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
292 288 291 bitrd ⊢ ( 𝐶 ∈ On → ( ∅ ∈ 𝐶 ↔ ( ω ↑o ( ω ↑o ∅ ) ) ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
293 292 biimprd ⊢ ( 𝐶 ∈ On → ( ( ω ↑o ( ω ↑o ∅ ) ) ∈ ( ω ↑o ( ω ↑o 𝐶 ) ) → ∅ ∈ 𝐶 ) )
294 286 293 sylcom ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( 𝐶 ∈ On → ∅ ∈ 𝐶 ) )
295 eloni ⊢ ( 𝐶 ∈ On → Ord 𝐶 )
296 ordsucss ⊢ ( Ord 𝐶 → ( ∅ ∈ 𝐶 → suc ∅ ⊆ 𝐶 ) )
297 94 sseq1i ⊢ ( 1o ⊆ 𝐶 ↔ suc ∅ ⊆ 𝐶 )
298 296 297 imbitrrdi ⊢ ( Ord 𝐶 → ( ∅ ∈ 𝐶 → 1o ⊆ 𝐶 ) )
299 295 298 syl ⊢ ( 𝐶 ∈ On → ( ∅ ∈ 𝐶 → 1o ⊆ 𝐶 ) )
300 294 299 sylcom ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( 𝐶 ∈ On → 1o ⊆ 𝐶 ) )
301 266 300 jcai ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) )
302 33 a1i ⊢ ( 𝐶 ∈ On → ω ∈ On )
303 80 a1i ⊢ ( 𝐶 ∈ On → 1o ∈ On )
304 302 303 35 3jca ⊢ ( 𝐶 ∈ On → ( ω ∈ On ∧ 1o ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ) )
305 304 adantr ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → ( ω ∈ On ∧ 1o ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ) )
306 oeoa ⊢ ( ( ω ∈ On ∧ 1o ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ) → ( ω ↑o ( 1o +o ( ω ↑o 𝐶 ) ) ) = ( ( ω ↑o 1o ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
307 305 306 syl ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → ( ω ↑o ( 1o +o ( ω ↑o 𝐶 ) ) ) = ( ( ω ↑o 1o ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
308 63 a1i ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → 1o ∈ ω )
309 35 adantr ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → ( ω ↑o 𝐶 ) ∈ On )
310 oeword ⊢ ( ( 1o ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ ( On ∖ 2o ) ) → ( 1o ⊆ 𝐶 ↔ ( ω ↑o 1o ) ⊆ ( ω ↑o 𝐶 ) ) )
311 80 65 310 mp3an13 ⊢ ( 𝐶 ∈ On → ( 1o ⊆ 𝐶 ↔ ( ω ↑o 1o ) ⊆ ( ω ↑o 𝐶 ) ) )
312 311 biimpa ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → ( ω ↑o 1o ) ⊆ ( ω ↑o 𝐶 ) )
313 163 312 eqsstrrid ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → ω ⊆ ( ω ↑o 𝐶 ) )
314 oaabs ⊢ ( ( ( 1o ∈ ω ∧ ( ω ↑o 𝐶 ) ∈ On ) ∧ ω ⊆ ( ω ↑o 𝐶 ) ) → ( 1o +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
315 308 309 313 314 syl21anc ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → ( 1o +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
316 315 oveq2d ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → ( ω ↑o ( 1o +o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
317 307 316 eqtr3d ⊢ ( ( 𝐶 ∈ On ∧ 1o ⊆ 𝐶 ) → ( ( ω ↑o 1o ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
318 301 317 syl ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( ( ω ↑o 1o ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
319 265 318 eqtrd ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ 𝑥 = ∅ ) → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
320 245 196 197 3syl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ∅ ∈ 𝑥 → suc ∅ ⊆ 𝑥 ) )
321 320 imp ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → suc ∅ ⊆ 𝑥 )
322 94 321 eqsstrid ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → 1o ⊆ 𝑥 )
323 248 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → 𝑥 ∈ ( ω ↑o 𝐶 ) )
324 242 323 228 syl2an2r ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → 𝑥 ∈ On )
325 65 a1i ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ω ∈ ( On ∖ 2o ) )
326 oeword ⊢ ( ( 1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ ( On ∖ 2o ) ) → ( 1o ⊆ 𝑥 ↔ ( ω ↑o 1o ) ⊆ ( ω ↑o 𝑥 ) ) )
327 80 324 325 326 mp3an2i ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( 1o ⊆ 𝑥 ↔ ( ω ↑o 1o ) ⊆ ( ω ↑o 𝑥 ) ) )
328 322 327 mpbid ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( ω ↑o 1o ) ⊆ ( ω ↑o 𝑥 ) )
329 163 328 eqsstrrid ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ω ⊆ ( ω ↑o 𝑥 ) )
330 ssequn1 ⊢ ( ω ⊆ ( ω ↑o 𝑥 ) ↔ ( ω ∪ ( ω ↑o 𝑥 ) ) = ( ω ↑o 𝑥 ) )
331 329 330 sylib ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( ω ∪ ( ω ↑o 𝑥 ) ) = ( ω ↑o 𝑥 ) )
332 331 oveq1d ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ( ω ↑o 𝑥 ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
333 242 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( ω ↑o 𝐶 ) ∈ On )
334 oeoa ⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ) → ( ω ↑o ( 𝑥 +o ( ω ↑o 𝐶 ) ) ) = ( ( ω ↑o 𝑥 ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
335 33 324 333 334 mp3an2i ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( ω ↑o ( 𝑥 +o ( ω ↑o 𝐶 ) ) ) = ( ( ω ↑o 𝑥 ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
336 ssidd ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( ω ↑o 𝐶 ) ⊆ ( ω ↑o 𝐶 ) )
337 323 333 336 250 syl21anc ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( 𝑥 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
338 337 oveq2d ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( ω ↑o ( 𝑥 +o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
339 332 335 338 3eqtr2d ⊢ ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) ∧ ∅ ∈ 𝑥 ) → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
340 227 229 202 3syl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝑥 = ∅ ∨ ∅ ∈ 𝑥 ) )
341 319 339 340 mpjaodan ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
342 277 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 )
343 33 229 75 sylancr ⊢ ( ( 𝐶 ∈ On ∧ 𝑥 ∈ ( ω ↑o 𝐶 ) ) → ( ω ↑o 𝑥 ) ∈ On )
344 343 33 jctil ⊢ ( ( 𝐶 ∈ On ∧ 𝑥 ∈ ( ω ↑o 𝐶 ) ) → ( ω ∈ On ∧ ( ω ↑o 𝑥 ) ∈ On ) )
345 onun2 ⊢ ( ( ω ∈ On ∧ ( ω ↑o 𝑥 ) ∈ On ) → ( ω ∪ ( ω ↑o 𝑥 ) ) ∈ On )
346 227 344 345 3syl ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ∪ ( ω ↑o 𝑥 ) ) ∈ On )
347 omwordri ⊢ ( ( ( ω ∪ ( ω ↑o 𝑥 ) ) ∈ On ∧ 𝐴 ∈ On ∧ ( ω ↑o ( ω ↑o 𝐶 ) ) ∈ On ) → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ⊆ ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ) )
348 346 224 237 347 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ⊆ ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ) )
349 342 348 mpd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ( ω ∪ ( ω ↑o 𝑥 ) ) ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) ⊆ ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
350 341 349 eqsstrrd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ω ↑o ( ω ↑o 𝐶 ) ) ⊆ ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
351 256 350 eqssd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) )
352 49 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( ( 𝐴 ·o 𝐵 ) = 𝐵 ↔ ( 𝐴 ·o ( ω ↑o ( ω ↑o 𝐶 ) ) ) = ( ω ↑o ( ω ↑o 𝐶 ) ) ) )
353 351 352 mpbird ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) ) → ( 𝐴 ·o 𝐵 ) = 𝐵 )
354 353 ex ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) → ( ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
355 354 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( ( 𝑥 ∈ ( ω ↑o 𝐶 ) ∧ ( ω ∪ ( ω ↑o 𝑥 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ω ↑o ( 𝑥 +o 𝑥 ) ) ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
356 141 143 222 355 mp3and ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝐴 ·o 𝐵 ) = 𝐵 )
357 356 ex ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) ∧ 𝑥 ∈ On ) ∧ 𝑦 ∈ ( ω ∖ 1o ) ) ∧ 𝑧 ∈ ( ω ↑o 𝑥 ) ) → ( ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
358 71 357 syl5 ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑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 rexlimdva ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( ω ∖ 1o ) ∃ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
362 361 exlimdv ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) → ( ∃ 𝑤 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( ω ∖ 1o ) ∃ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
363 70 362 syl5 ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) → ( ∃! 𝑤 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( ω ∖ 1o ) ∃ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝑤 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o 𝑧 ) = 𝐴 ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
364 69 363 mpd ⊢ ( ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ∧ ω ⊆ 𝐴 ) → ( 𝐴 ·o 𝐵 ) = 𝐵 )
365 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
366 59 365 syl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) → Ord 𝐴 )
367 ordtri2or ⊢ ( ( Ord 𝐴 ∧ Ord ω ) → ( 𝐴 ∈ ω ∨ ω ⊆ 𝐴 ) )
368 366 158 367 sylancl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) → ( 𝐴 ∈ ω ∨ ω ⊆ 𝐴 ) )
369 51 364 368 mpjaodan ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) → ( 𝐴 ·o 𝐵 ) = 𝐵 )
370 369 ex ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) → ( ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
371 6 30 370 3jaod ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) → ( ( 𝐵 = ∅ ∨ 𝐵 = 2o ∨ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) → ( 𝐴 ·o 𝐵 ) = 𝐵 ) )
372 371 imp ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 = ∅ ∨ 𝐵 = 2o ∨ ( 𝐵 = ( ω ↑o ( ω ↑o 𝐶 ) ) ∧ 𝐶 ∈ On ) ) ) → ( 𝐴 ·o 𝐵 ) = 𝐵 )