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 ordirr 
 |-  ( Ord _om -> -. _om e. _om )
192 158 191 ax-mp 
 |-  -. _om e. _om
193 192 pm2.21i 
 |-  ( _om e. _om -> 1o C_ x )
194 193 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 ) )
195 186 190 194 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 ) )
196 eloni 
 |-  ( x e. On -> Ord x )
197 ordsucss 
 |-  ( Ord x -> ( (/) e. x -> suc (/) C_ x ) )
198 197 imp 
 |-  ( ( Ord x /\ (/) e. x ) -> suc (/) C_ x )
199 94 198 eqsstrid 
 |-  ( ( Ord x /\ (/) e. x ) -> 1o C_ x )
200 199 ex 
 |-  ( Ord x -> ( (/) e. x -> 1o C_ x ) )
201 106 196 200 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 ) )
202 on0eqel 
 |-  ( x e. On -> ( x = (/) \/ (/) e. x ) )
203 106 202 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 ) )
204 195 201 203 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 )
205 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 )
206 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 )
207 205 106 206 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 ) )
208 oewordi 
 |-  ( ( ( 1o e. On /\ x e. On /\ _om e. On ) /\ (/) e. _om ) -> ( 1o C_ x -> ( _om ^o 1o ) C_ ( _om ^o x ) ) )
209 207 39 208 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 ) ) )
210 204 209 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 ) )
211 163 210 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 ) )
212 161 211 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 ) )
213 onsuc 
 |-  ( y e. On -> suc y e. On )
214 111 213 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 )
215 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 ) ) ) )
216 214 107 107 215 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 ) ) ) )
217 212 216 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 ) ) )
218 157 217 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 ) ) )
219 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 ) )
220 oeoa 
 |-  ( ( _om e. On /\ x e. On /\ x e. On ) -> ( _om ^o ( x +o x ) ) = ( ( _om ^o x ) .o ( _om ^o x ) ) )
221 33 106 106 220 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 ) ) )
222 218 219 221 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 ) ) )
223 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 ) ) )
224 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 )
225 simprr 
 |-  ( ( ( A e. B /\ (/) e. A ) /\ ( B = ( _om ^o ( _om ^o C ) ) /\ C e. On ) ) -> C e. On )
226 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 ) )
227 225 226 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 ) ) )
228 onelon 
 |-  ( ( ( _om ^o C ) e. On /\ x e. ( _om ^o C ) ) -> x e. On )
229 35 228 sylan 
 |-  ( ( C e. On /\ x e. ( _om ^o C ) ) -> x e. On )
230 pm4.24 
 |-  ( x e. On <-> ( x e. On /\ x e. On ) )
231 229 230 sylib 
 |-  ( ( C e. On /\ x e. ( _om ^o C ) ) -> ( x e. On /\ x e. On ) )
232 oacl 
 |-  ( ( x e. On /\ x e. On ) -> ( x +o x ) e. On )
233 231 232 syl 
 |-  ( ( C e. On /\ x e. ( _om ^o C ) ) -> ( x +o x ) e. On )
234 oecl 
 |-  ( ( _om e. On /\ ( x +o x ) e. On ) -> ( _om ^o ( x +o x ) ) e. On )
235 33 233 234 sylancr 
 |-  ( ( C e. On /\ x e. ( _om ^o C ) ) -> ( _om ^o ( x +o x ) ) e. On )
236 227 235 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 )
237 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 )
238 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 ) ) ) ) )
239 224 236 237 238 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 ) ) ) ) )
240 223 239 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 ) ) ) )
241 227 231 232 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 )
242 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 )
243 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 ) ) ) )
244 33 241 242 243 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 ) ) ) )
245 227 229 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 )
246 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 ) ) ) )
247 245 245 242 246 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 ) ) ) )
248 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 ) )
249 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 ) )
250 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 ) )
251 248 242 249 250 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 ) )
252 251 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 ) ) )
253 247 252 251 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 ) )
254 253 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 ) ) )
255 244 254 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 ) ) )
256 240 255 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 ) ) )
257 oveq2 
 |-  ( x = (/) -> ( _om ^o x ) = ( _om ^o (/) ) )
258 257 167 eqtrdi 
 |-  ( x = (/) -> ( _om ^o x ) = 1o )
259 258 uneq2d 
 |-  ( x = (/) -> ( _om u. ( _om ^o x ) ) = ( _om u. 1o ) )
260 33 oneluni 
 |-  ( 1o e. _om -> ( _om u. 1o ) = _om )
261 63 260 ax-mp 
 |-  ( _om u. 1o ) = _om
262 261 163 eqtr4i 
 |-  ( _om u. 1o ) = ( _om ^o 1o )
263 259 262 eqtrdi 
 |-  ( x = (/) -> ( _om u. ( _om ^o x ) ) = ( _om ^o 1o ) )
264 263 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 ) )
265 264 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 ) ) ) )
266 225 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 )
267 oecl 
 |-  ( ( _om e. On /\ (/) e. On ) -> ( _om ^o (/) ) e. On )
268 33 73 267 mp2an 
 |-  ( _om ^o (/) ) e. On
269 oecl 
 |-  ( ( _om e. On /\ ( _om ^o (/) ) e. On ) -> ( _om ^o ( _om ^o (/) ) ) e. On )
270 33 268 269 mp2an 
 |-  ( _om ^o ( _om ^o (/) ) ) e. On
271 270 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 ) )
272 271 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 ) ) )
273 167 oveq2i 
 |-  ( _om ^o ( _om ^o (/) ) ) = ( _om ^o 1o )
274 273 163 eqtri 
 |-  ( _om ^o ( _om ^o (/) ) ) = _om
275 ssun1 
 |-  _om C_ ( _om u. ( _om ^o x ) )
276 274 275 eqsstri 
 |-  ( _om ^o ( _om ^o (/) ) ) C_ ( _om u. ( _om ^o x ) )
277 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 )
278 276 277 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 )
279 278 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 )
280 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 )
281 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 ) ) )
282 280 281 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 ) ) )
283 279 282 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 ) ) ) )
284 283 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 ) ) ) )
285 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 ) ) ) )
286 272 284 285 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 ) ) ) )
287 oeord 
 |-  ( ( (/) e. On /\ C e. On /\ _om e. ( On \ 2o ) ) -> ( (/) e. C <-> ( _om ^o (/) ) e. ( _om ^o C ) ) )
288 73 65 287 mp3an13 
 |-  ( C e. On -> ( (/) e. C <-> ( _om ^o (/) ) e. ( _om ^o C ) ) )
289 65 a1i 
 |-  ( C e. On -> _om e. ( On \ 2o ) )
290 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 ) ) ) )
291 268 35 289 290 mp3an2i 
 |-  ( C e. On -> ( ( _om ^o (/) ) e. ( _om ^o C ) <-> ( _om ^o ( _om ^o (/) ) ) e. ( _om ^o ( _om ^o C ) ) ) )
292 288 291 bitrd 
 |-  ( C e. On -> ( (/) e. C <-> ( _om ^o ( _om ^o (/) ) ) e. ( _om ^o ( _om ^o C ) ) ) )
293 292 biimprd 
 |-  ( C e. On -> ( ( _om ^o ( _om ^o (/) ) ) e. ( _om ^o ( _om ^o C ) ) -> (/) e. C ) )
294 286 293 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 ) )
295 eloni 
 |-  ( C e. On -> Ord C )
296 ordsucss 
 |-  ( Ord C -> ( (/) e. C -> suc (/) C_ C ) )
297 94 sseq1i 
 |-  ( 1o C_ C <-> suc (/) C_ C )
298 296 297 imbitrrdi 
 |-  ( Ord C -> ( (/) e. C -> 1o C_ C ) )
299 295 298 syl 
 |-  ( C e. On -> ( (/) e. C -> 1o C_ C ) )
300 294 299 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 ) )
301 266 300 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 ) )
302 33 a1i 
 |-  ( C e. On -> _om e. On )
303 80 a1i 
 |-  ( C e. On -> 1o e. On )
304 302 303 35 3jca 
 |-  ( C e. On -> ( _om e. On /\ 1o e. On /\ ( _om ^o C ) e. On ) )
305 304 adantr 
 |-  ( ( C e. On /\ 1o C_ C ) -> ( _om e. On /\ 1o e. On /\ ( _om ^o C ) e. On ) )
306 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 ) ) ) )
307 305 306 syl 
 |-  ( ( C e. On /\ 1o C_ C ) -> ( _om ^o ( 1o +o ( _om ^o C ) ) ) = ( ( _om ^o 1o ) .o ( _om ^o ( _om ^o C ) ) ) )
308 63 a1i 
 |-  ( ( C e. On /\ 1o C_ C ) -> 1o e. _om )
309 35 adantr 
 |-  ( ( C e. On /\ 1o C_ C ) -> ( _om ^o C ) e. On )
310 oeword 
 |-  ( ( 1o e. On /\ C e. On /\ _om e. ( On \ 2o ) ) -> ( 1o C_ C <-> ( _om ^o 1o ) C_ ( _om ^o C ) ) )
311 80 65 310 mp3an13 
 |-  ( C e. On -> ( 1o C_ C <-> ( _om ^o 1o ) C_ ( _om ^o C ) ) )
312 311 biimpa 
 |-  ( ( C e. On /\ 1o C_ C ) -> ( _om ^o 1o ) C_ ( _om ^o C ) )
313 163 312 eqsstrrid 
 |-  ( ( C e. On /\ 1o C_ C ) -> _om C_ ( _om ^o C ) )
314 oaabs 
 |-  ( ( ( 1o e. _om /\ ( _om ^o C ) e. On ) /\ _om C_ ( _om ^o C ) ) -> ( 1o +o ( _om ^o C ) ) = ( _om ^o C ) )
315 308 309 313 314 syl21anc 
 |-  ( ( C e. On /\ 1o C_ C ) -> ( 1o +o ( _om ^o C ) ) = ( _om ^o C ) )
316 315 oveq2d 
 |-  ( ( C e. On /\ 1o C_ C ) -> ( _om ^o ( 1o +o ( _om ^o C ) ) ) = ( _om ^o ( _om ^o C ) ) )
317 307 316 eqtr3d 
 |-  ( ( C e. On /\ 1o C_ C ) -> ( ( _om ^o 1o ) .o ( _om ^o ( _om ^o C ) ) ) = ( _om ^o ( _om ^o C ) ) )
318 301 317 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 ) ) )
319 265 318 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 ) ) )
320 245 196 197 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 ) )
321 320 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 )
322 94 321 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 )
323 248 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 ) )
324 242 323 228 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 )
325 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 ) )
326 oeword 
 |-  ( ( 1o e. On /\ x e. On /\ _om e. ( On \ 2o ) ) -> ( 1o C_ x <-> ( _om ^o 1o ) C_ ( _om ^o x ) ) )
327 80 324 325 326 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 ) ) )
328 322 327 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 ) )
329 163 328 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 ) )
330 ssequn1 
 |-  ( _om C_ ( _om ^o x ) <-> ( _om u. ( _om ^o x ) ) = ( _om ^o x ) )
331 329 330 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 ) )
332 331 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 ) ) ) )
333 242 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 )
334 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 ) ) ) )
335 33 324 333 334 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 ) ) ) )
336 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 ) )
337 323 333 336 250 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 ) )
338 337 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 ) ) )
339 332 335 338 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 ) ) )
340 227 229 202 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 ) )
341 319 339 340 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 ) ) )
342 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 u. ( _om ^o x ) ) C_ A )
343 33 229 75 sylancr 
 |-  ( ( C e. On /\ x e. ( _om ^o C ) ) -> ( _om ^o x ) e. On )
344 343 33 jctil 
 |-  ( ( C e. On /\ x e. ( _om ^o C ) ) -> ( _om e. On /\ ( _om ^o x ) e. On ) )
345 onun2 
 |-  ( ( _om e. On /\ ( _om ^o x ) e. On ) -> ( _om u. ( _om ^o x ) ) e. On )
346 227 344 345 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 )
347 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 ) ) ) ) )
348 346 224 237 347 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 ) ) ) ) )
349 342 348 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 ) ) ) )
350 341 349 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 ) ) ) )
351 256 350 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 ) ) )
352 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 ) ) ) )
353 351 352 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 )
354 353 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 ) )
355 354 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 ) )
356 141 143 222 355 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 )
357 356 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 ) )
358 71 357 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 ) )
359 358 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 ) )
360 359 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 ) )
361 360 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 ) )
362 361 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 ) )
363 70 362 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 ) )
364 69 363 mpd 
 |-  ( ( ( ( A e. B /\ (/) e. A ) /\ ( B = ( _om ^o ( _om ^o C ) ) /\ C e. On ) ) /\ _om C_ A ) -> ( A .o B ) = B )
365 eloni 
 |-  ( A e. On -> Ord A )
366 59 365 syl 
 |-  ( ( ( A e. B /\ (/) e. A ) /\ ( B = ( _om ^o ( _om ^o C ) ) /\ C e. On ) ) -> Ord A )
367 ordtri2or 
 |-  ( ( Ord A /\ Ord _om ) -> ( A e. _om \/ _om C_ A ) )
368 366 158 367 sylancl 
 |-  ( ( ( A e. B /\ (/) e. A ) /\ ( B = ( _om ^o ( _om ^o C ) ) /\ C e. On ) ) -> ( A e. _om \/ _om C_ A ) )
369 51 364 368 mpjaodan 
 |-  ( ( ( A e. B /\ (/) e. A ) /\ ( B = ( _om ^o ( _om ^o C ) ) /\ C e. On ) ) -> ( A .o B ) = B )
370 369 ex 
 |-  ( ( A e. B /\ (/) e. A ) -> ( ( B = ( _om ^o ( _om ^o C ) ) /\ C e. On ) -> ( A .o B ) = B ) )
371 6 30 370 3jaod 
 |-  ( ( A e. B /\ (/) e. A ) -> ( ( B = (/) \/ B = 2o \/ ( B = ( _om ^o ( _om ^o C ) ) /\ C e. On ) ) -> ( A .o B ) = B ) )
372 371 imp 
 |-  ( ( ( A e. B /\ (/) e. A ) /\ ( B = (/) \/ B = 2o \/ ( B = ( _om ^o ( _om ^o C ) ) /\ C e. On ) ) ) -> ( A .o B ) = B )