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 
|- ( ( ( A e. B /\ (/) e. A ) /\ ( B = (/) \/ B = 2o \/ ( B = ( _om ^o ( _om ^o C ) ) /\ C e. On ) ) ) -> ( A .o B ) = B )

Proof

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