Metamath Proof Explorer

Theorem oeeui

Description: The division algorithm for ordinal exponentiation. (This version of oeeu gives an explicit expression for the unique solution of the equation, in terms of the solution P to omeu .) (Contributed by Mario Carneiro, 25-May-2015)

Ref Expression
Hypotheses oeeu.1 
|- X = U. |^| { x e. On | B e. ( A ^o x ) }
oeeu.2 
|- P = ( iota w E. y e. On E. z e. ( A ^o X ) ( w = <. y , z >. /\ ( ( ( A ^o X ) .o y ) +o z ) = B ) )
oeeu.3 
|- Y = ( 1st ` P )
oeeu.4 
|- Z = ( 2nd ` P )
Assertion oeeui 
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( ( ( C e. On /\ D e. ( A \ 1o ) /\ E e. ( A ^o C ) ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) <-> ( C = X /\ D = Y /\ E = Z ) ) )

Proof

Step Hyp Ref Expression
1 oeeu.1 
 |-  X = U. |^| { x e. On | B e. ( A ^o x ) }
2 oeeu.2 
 |-  P = ( iota w E. y e. On E. z e. ( A ^o X ) ( w = <. y , z >. /\ ( ( ( A ^o X ) .o y ) +o z ) = B ) )
3 oeeu.3 
 |-  Y = ( 1st ` P )
4 oeeu.4 
 |-  Z = ( 2nd ` P )
5 eldifi 
 |-  ( A e. ( On \ 2o ) -> A e. On )
6 5 adantr 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> A e. On )
7 6 ad2antrr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> A e. On )
8 simprl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> C e. On )
9 oecl 
 |-  ( ( A e. On /\ C e. On ) -> ( A ^o C ) e. On )
10 7 8 9 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( A ^o C ) e. On )
11 om1 
 |-  ( ( A ^o C ) e. On -> ( ( A ^o C ) .o 1o ) = ( A ^o C ) )
12 10 11 syl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( ( A ^o C ) .o 1o ) = ( A ^o C ) )
13 df1o2 
 |-  1o = { (/) }
14 dif1o 
 |-  ( D e. ( A \ 1o ) <-> ( D e. A /\ D =/= (/) ) )
15 14 simprbi 
 |-  ( D e. ( A \ 1o ) -> D =/= (/) )
16 15 ad2antll 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> D =/= (/) )
17 eldifi 
 |-  ( D e. ( A \ 1o ) -> D e. A )
18 17 ad2antll 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> D e. A )
19 onelon 
 |-  ( ( A e. On /\ D e. A ) -> D e. On )
20 7 18 19 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> D e. On )
21 on0eln0 
 |-  ( D e. On -> ( (/) e. D <-> D =/= (/) ) )
22 20 21 syl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( (/) e. D <-> D =/= (/) ) )
23 16 22 mpbird 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> (/) e. D )
24 23 snssd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> { (/) } C_ D )
25 13 24 eqsstrid 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> 1o C_ D )
26 1on 
 |-  1o e. On
27 26 a1i 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> 1o e. On )
28 omwordi 
 |-  ( ( 1o e. On /\ D e. On /\ ( A ^o C ) e. On ) -> ( 1o C_ D -> ( ( A ^o C ) .o 1o ) C_ ( ( A ^o C ) .o D ) ) )
29 27 20 10 28 syl3anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( 1o C_ D -> ( ( A ^o C ) .o 1o ) C_ ( ( A ^o C ) .o D ) ) )
30 25 29 mpd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( ( A ^o C ) .o 1o ) C_ ( ( A ^o C ) .o D ) )
31 12 30 eqsstrrd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( A ^o C ) C_ ( ( A ^o C ) .o D ) )
32 omcl 
 |-  ( ( ( A ^o C ) e. On /\ D e. On ) -> ( ( A ^o C ) .o D ) e. On )
33 10 20 32 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( ( A ^o C ) .o D ) e. On )
34 simplrl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> E e. ( A ^o C ) )
35 onelon 
 |-  ( ( ( A ^o C ) e. On /\ E e. ( A ^o C ) ) -> E e. On )
36 10 34 35 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> E e. On )
37 oaword1 
 |-  ( ( ( ( A ^o C ) .o D ) e. On /\ E e. On ) -> ( ( A ^o C ) .o D ) C_ ( ( ( A ^o C ) .o D ) +o E ) )
38 33 36 37 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( ( A ^o C ) .o D ) C_ ( ( ( A ^o C ) .o D ) +o E ) )
39 simplrr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( ( ( A ^o C ) .o D ) +o E ) = B )
40 38 39 sseqtrd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( ( A ^o C ) .o D ) C_ B )
41 31 40 sstrd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( A ^o C ) C_ B )
42 1 oeeulem 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( X e. On /\ ( A ^o X ) C_ B /\ B e. ( A ^o suc X ) ) )
43 42 simp3d 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> B e. ( A ^o suc X ) )
44 43 ad2antrr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> B e. ( A ^o suc X ) )
45 42 simp1d 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> X e. On )
46 45 ad2antrr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> X e. On )
47 onsuc 
 |-  ( X e. On -> suc X e. On )
48 46 47 syl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> suc X e. On )
49 oecl 
 |-  ( ( A e. On /\ suc X e. On ) -> ( A ^o suc X ) e. On )
50 7 48 49 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( A ^o suc X ) e. On )
51 ontr2 
 |-  ( ( ( A ^o C ) e. On /\ ( A ^o suc X ) e. On ) -> ( ( ( A ^o C ) C_ B /\ B e. ( A ^o suc X ) ) -> ( A ^o C ) e. ( A ^o suc X ) ) )
52 10 50 51 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( ( ( A ^o C ) C_ B /\ B e. ( A ^o suc X ) ) -> ( A ^o C ) e. ( A ^o suc X ) ) )
53 41 44 52 mp2and 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( A ^o C ) e. ( A ^o suc X ) )
54 simplll 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> A e. ( On \ 2o ) )
55 oeord 
 |-  ( ( C e. On /\ suc X e. On /\ A e. ( On \ 2o ) ) -> ( C e. suc X <-> ( A ^o C ) e. ( A ^o suc X ) ) )
56 8 48 54 55 syl3anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( C e. suc X <-> ( A ^o C ) e. ( A ^o suc X ) ) )
57 53 56 mpbird 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> C e. suc X )
58 onsssuc 
 |-  ( ( C e. On /\ X e. On ) -> ( C C_ X <-> C e. suc X ) )
59 8 46 58 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( C C_ X <-> C e. suc X ) )
60 57 59 mpbird 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> C C_ X )
61 42 simp2d 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( A ^o X ) C_ B )
62 61 ad2antrr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( A ^o X ) C_ B )
63 eloni 
 |-  ( A e. On -> Ord A )
64 7 63 syl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> Ord A )
65 ordsucss 
 |-  ( Ord A -> ( D e. A -> suc D C_ A ) )
66 64 18 65 sylc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> suc D C_ A )
67 onsuc 
 |-  ( D e. On -> suc D e. On )
68 20 67 syl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> suc D e. On )
69 dif20el 
 |-  ( A e. ( On \ 2o ) -> (/) e. A )
70 54 69 syl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> (/) e. A )
71 oen0 
 |-  ( ( ( A e. On /\ C e. On ) /\ (/) e. A ) -> (/) e. ( A ^o C ) )
72 7 8 70 71 syl21anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> (/) e. ( A ^o C ) )
73 omword 
 |-  ( ( ( suc D e. On /\ A e. On /\ ( A ^o C ) e. On ) /\ (/) e. ( A ^o C ) ) -> ( suc D C_ A <-> ( ( A ^o C ) .o suc D ) C_ ( ( A ^o C ) .o A ) ) )
74 68 7 10 72 73 syl31anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( suc D C_ A <-> ( ( A ^o C ) .o suc D ) C_ ( ( A ^o C ) .o A ) ) )
75 66 74 mpbid 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( ( A ^o C ) .o suc D ) C_ ( ( A ^o C ) .o A ) )
76 oaord 
 |-  ( ( E e. On /\ ( A ^o C ) e. On /\ ( ( A ^o C ) .o D ) e. On ) -> ( E e. ( A ^o C ) <-> ( ( ( A ^o C ) .o D ) +o E ) e. ( ( ( A ^o C ) .o D ) +o ( A ^o C ) ) ) )
77 36 10 33 76 syl3anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( E e. ( A ^o C ) <-> ( ( ( A ^o C ) .o D ) +o E ) e. ( ( ( A ^o C ) .o D ) +o ( A ^o C ) ) ) )
78 34 77 mpbid 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( ( ( A ^o C ) .o D ) +o E ) e. ( ( ( A ^o C ) .o D ) +o ( A ^o C ) ) )
79 39 78 eqeltrrd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> B e. ( ( ( A ^o C ) .o D ) +o ( A ^o C ) ) )
80 odi 
 |-  ( ( ( A ^o C ) e. On /\ D e. On /\ 1o e. On ) -> ( ( A ^o C ) .o ( D +o 1o ) ) = ( ( ( A ^o C ) .o D ) +o ( ( A ^o C ) .o 1o ) ) )
81 10 20 27 80 syl3anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( ( A ^o C ) .o ( D +o 1o ) ) = ( ( ( A ^o C ) .o D ) +o ( ( A ^o C ) .o 1o ) ) )
82 oa1suc 
 |-  ( D e. On -> ( D +o 1o ) = suc D )
83 20 82 syl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( D +o 1o ) = suc D )
84 83 oveq2d 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( ( A ^o C ) .o ( D +o 1o ) ) = ( ( A ^o C ) .o suc D ) )
85 12 oveq2d 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( ( ( A ^o C ) .o D ) +o ( ( A ^o C ) .o 1o ) ) = ( ( ( A ^o C ) .o D ) +o ( A ^o C ) ) )
86 81 84 85 3eqtr3d 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( ( A ^o C ) .o suc D ) = ( ( ( A ^o C ) .o D ) +o ( A ^o C ) ) )
87 79 86 eleqtrrd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> B e. ( ( A ^o C ) .o suc D ) )
88 75 87 sseldd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> B e. ( ( A ^o C ) .o A ) )
89 oesuc 
 |-  ( ( A e. On /\ C e. On ) -> ( A ^o suc C ) = ( ( A ^o C ) .o A ) )
90 7 8 89 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( A ^o suc C ) = ( ( A ^o C ) .o A ) )
91 88 90 eleqtrrd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> B e. ( A ^o suc C ) )
92 oecl 
 |-  ( ( A e. On /\ X e. On ) -> ( A ^o X ) e. On )
93 7 46 92 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( A ^o X ) e. On )
94 onsuc 
 |-  ( C e. On -> suc C e. On )
95 94 ad2antrl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> suc C e. On )
96 oecl 
 |-  ( ( A e. On /\ suc C e. On ) -> ( A ^o suc C ) e. On )
97 7 95 96 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( A ^o suc C ) e. On )
98 ontr2 
 |-  ( ( ( A ^o X ) e. On /\ ( A ^o suc C ) e. On ) -> ( ( ( A ^o X ) C_ B /\ B e. ( A ^o suc C ) ) -> ( A ^o X ) e. ( A ^o suc C ) ) )
99 93 97 98 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( ( ( A ^o X ) C_ B /\ B e. ( A ^o suc C ) ) -> ( A ^o X ) e. ( A ^o suc C ) ) )
100 62 91 99 mp2and 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( A ^o X ) e. ( A ^o suc C ) )
101 oeord 
 |-  ( ( X e. On /\ suc C e. On /\ A e. ( On \ 2o ) ) -> ( X e. suc C <-> ( A ^o X ) e. ( A ^o suc C ) ) )
102 46 95 54 101 syl3anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( X e. suc C <-> ( A ^o X ) e. ( A ^o suc C ) ) )
103 100 102 mpbird 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> X e. suc C )
104 onsssuc 
 |-  ( ( X e. On /\ C e. On ) -> ( X C_ C <-> X e. suc C ) )
105 46 8 104 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( X C_ C <-> X e. suc C ) )
106 103 105 mpbird 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> X C_ C )
107 60 106 eqssd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> C = X )
108 107 20 jca 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C e. On /\ D e. ( A \ 1o ) ) ) -> ( C = X /\ D e. On ) )
109 simprl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> C = X )
110 45 ad2antrr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> X e. On )
111 109 110 eqeltrd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> C e. On )
112 6 ad2antrr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> A e. On )
113 112 111 9 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( A ^o C ) e. On )
114 simprr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> D e. On )
115 113 114 32 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( ( A ^o C ) .o D ) e. On )
116 simplrl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> E e. ( A ^o C ) )
117 113 116 35 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> E e. On )
118 115 117 37 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( ( A ^o C ) .o D ) C_ ( ( ( A ^o C ) .o D ) +o E ) )
119 simplrr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( ( ( A ^o C ) .o D ) +o E ) = B )
120 118 119 sseqtrd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( ( A ^o C ) .o D ) C_ B )
121 43 ad2antrr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> B e. ( A ^o suc X ) )
122 suceq 
 |-  ( C = X -> suc C = suc X )
123 122 ad2antrl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> suc C = suc X )
124 123 oveq2d 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( A ^o suc C ) = ( A ^o suc X ) )
125 112 111 89 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( A ^o suc C ) = ( ( A ^o C ) .o A ) )
126 124 125 eqtr3d 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( A ^o suc X ) = ( ( A ^o C ) .o A ) )
127 121 126 eleqtrd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> B e. ( ( A ^o C ) .o A ) )
128 omcl 
 |-  ( ( ( A ^o C ) e. On /\ A e. On ) -> ( ( A ^o C ) .o A ) e. On )
129 113 112 128 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( ( A ^o C ) .o A ) e. On )
130 ontr2 
 |-  ( ( ( ( A ^o C ) .o D ) e. On /\ ( ( A ^o C ) .o A ) e. On ) -> ( ( ( ( A ^o C ) .o D ) C_ B /\ B e. ( ( A ^o C ) .o A ) ) -> ( ( A ^o C ) .o D ) e. ( ( A ^o C ) .o A ) ) )
131 115 129 130 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( ( ( ( A ^o C ) .o D ) C_ B /\ B e. ( ( A ^o C ) .o A ) ) -> ( ( A ^o C ) .o D ) e. ( ( A ^o C ) .o A ) ) )
132 120 127 131 mp2and 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( ( A ^o C ) .o D ) e. ( ( A ^o C ) .o A ) )
133 69 adantr 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> (/) e. A )
134 133 ad2antrr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> (/) e. A )
135 112 111 134 71 syl21anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> (/) e. ( A ^o C ) )
136 omord2 
 |-  ( ( ( D e. On /\ A e. On /\ ( A ^o C ) e. On ) /\ (/) e. ( A ^o C ) ) -> ( D e. A <-> ( ( A ^o C ) .o D ) e. ( ( A ^o C ) .o A ) ) )
137 114 112 113 135 136 syl31anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( D e. A <-> ( ( A ^o C ) .o D ) e. ( ( A ^o C ) .o A ) ) )
138 132 137 mpbird 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> D e. A )
139 109 oveq2d 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( A ^o C ) = ( A ^o X ) )
140 61 ad2antrr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( A ^o X ) C_ B )
141 139 140 eqsstrd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( A ^o C ) C_ B )
142 eldifi 
 |-  ( B e. ( On \ 1o ) -> B e. On )
143 142 adantl 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> B e. On )
144 143 ad2antrr 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> B e. On )
145 ontri1 
 |-  ( ( ( A ^o C ) e. On /\ B e. On ) -> ( ( A ^o C ) C_ B <-> -. B e. ( A ^o C ) ) )
146 113 144 145 syl2anc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( ( A ^o C ) C_ B <-> -. B e. ( A ^o C ) ) )
147 141 146 mpbid 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> -. B e. ( A ^o C ) )
148 om0 
 |-  ( ( A ^o C ) e. On -> ( ( A ^o C ) .o (/) ) = (/) )
149 113 148 syl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( ( A ^o C ) .o (/) ) = (/) )
150 149 oveq1d 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( ( ( A ^o C ) .o (/) ) +o E ) = ( (/) +o E ) )
151 oa0r 
 |-  ( E e. On -> ( (/) +o E ) = E )
152 117 151 syl 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( (/) +o E ) = E )
153 150 152 eqtrd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( ( ( A ^o C ) .o (/) ) +o E ) = E )
154 153 116 eqeltrd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( ( ( A ^o C ) .o (/) ) +o E ) e. ( A ^o C ) )
155 oveq2 
 |-  ( D = (/) -> ( ( A ^o C ) .o D ) = ( ( A ^o C ) .o (/) ) )
156 155 oveq1d 
 |-  ( D = (/) -> ( ( ( A ^o C ) .o D ) +o E ) = ( ( ( A ^o C ) .o (/) ) +o E ) )
157 156 eleq1d 
 |-  ( D = (/) -> ( ( ( ( A ^o C ) .o D ) +o E ) e. ( A ^o C ) <-> ( ( ( A ^o C ) .o (/) ) +o E ) e. ( A ^o C ) ) )
158 154 157 syl5ibrcom 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( D = (/) -> ( ( ( A ^o C ) .o D ) +o E ) e. ( A ^o C ) ) )
159 119 eleq1d 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( ( ( ( A ^o C ) .o D ) +o E ) e. ( A ^o C ) <-> B e. ( A ^o C ) ) )
160 158 159 sylibd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( D = (/) -> B e. ( A ^o C ) ) )
161 160 necon3bd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( -. B e. ( A ^o C ) -> D =/= (/) ) )
162 147 161 mpd 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> D =/= (/) )
163 138 162 14 sylanbrc 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> D e. ( A \ 1o ) )
164 111 163 jca 
 |-  ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) /\ ( C = X /\ D e. On ) ) -> ( C e. On /\ D e. ( A \ 1o ) ) )
165 108 164 impbida 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) -> ( ( C e. On /\ D e. ( A \ 1o ) ) <-> ( C = X /\ D e. On ) ) )
166 165 ex 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) -> ( ( C e. On /\ D e. ( A \ 1o ) ) <-> ( C = X /\ D e. On ) ) ) )
167 166 pm5.32rd 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( ( ( C e. On /\ D e. ( A \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) <-> ( ( C = X /\ D e. On ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) ) )
168 anass 
 |-  ( ( ( C = X /\ D e. On ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) <-> ( C = X /\ ( D e. On /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) ) )
169 167 168 bitrdi 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( ( ( C e. On /\ D e. ( A \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) <-> ( C = X /\ ( D e. On /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) ) ) )
170 3anass 
 |-  ( ( D e. On /\ E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) <-> ( D e. On /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) )
171 oveq2 
 |-  ( C = X -> ( A ^o C ) = ( A ^o X ) )
172 171 eleq2d 
 |-  ( C = X -> ( E e. ( A ^o C ) <-> E e. ( A ^o X ) ) )
173 171 oveq1d 
 |-  ( C = X -> ( ( A ^o C ) .o D ) = ( ( A ^o X ) .o D ) )
174 173 oveq1d 
 |-  ( C = X -> ( ( ( A ^o C ) .o D ) +o E ) = ( ( ( A ^o X ) .o D ) +o E ) )
175 174 eqeq1d 
 |-  ( C = X -> ( ( ( ( A ^o C ) .o D ) +o E ) = B <-> ( ( ( A ^o X ) .o D ) +o E ) = B ) )
176 172 175 3anbi23d 
 |-  ( C = X -> ( ( D e. On /\ E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) <-> ( D e. On /\ E e. ( A ^o X ) /\ ( ( ( A ^o X ) .o D ) +o E ) = B ) ) )
177 170 176 bitr3id 
 |-  ( C = X -> ( ( D e. On /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) <-> ( D e. On /\ E e. ( A ^o X ) /\ ( ( ( A ^o X ) .o D ) +o E ) = B ) ) )
178 6 45 92 syl2anc 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( A ^o X ) e. On )
179 oen0 
 |-  ( ( ( A e. On /\ X e. On ) /\ (/) e. A ) -> (/) e. ( A ^o X ) )
180 6 45 133 179 syl21anc 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> (/) e. ( A ^o X ) )
181 180 ne0d 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( A ^o X ) =/= (/) )
182 omeu 
 |-  ( ( ( A ^o X ) e. On /\ B e. On /\ ( A ^o X ) =/= (/) ) -> E! a E. d e. On E. e e. ( A ^o X ) ( a = <. d , e >. /\ ( ( ( A ^o X ) .o d ) +o e ) = B ) )
183 opeq1 
 |-  ( y = d -> <. y , z >. = <. d , z >. )
184 183 eqeq2d 
 |-  ( y = d -> ( w = <. y , z >. <-> w = <. d , z >. ) )
185 oveq2 
 |-  ( y = d -> ( ( A ^o X ) .o y ) = ( ( A ^o X ) .o d ) )
186 185 oveq1d 
 |-  ( y = d -> ( ( ( A ^o X ) .o y ) +o z ) = ( ( ( A ^o X ) .o d ) +o z ) )
187 186 eqeq1d 
 |-  ( y = d -> ( ( ( ( A ^o X ) .o y ) +o z ) = B <-> ( ( ( A ^o X ) .o d ) +o z ) = B ) )
188 184 187 anbi12d 
 |-  ( y = d -> ( ( w = <. y , z >. /\ ( ( ( A ^o X ) .o y ) +o z ) = B ) <-> ( w = <. d , z >. /\ ( ( ( A ^o X ) .o d ) +o z ) = B ) ) )
189 opeq2 
 |-  ( z = e -> <. d , z >. = <. d , e >. )
190 189 eqeq2d 
 |-  ( z = e -> ( w = <. d , z >. <-> w = <. d , e >. ) )
191 oveq2 
 |-  ( z = e -> ( ( ( A ^o X ) .o d ) +o z ) = ( ( ( A ^o X ) .o d ) +o e ) )
192 191 eqeq1d 
 |-  ( z = e -> ( ( ( ( A ^o X ) .o d ) +o z ) = B <-> ( ( ( A ^o X ) .o d ) +o e ) = B ) )
193 190 192 anbi12d 
 |-  ( z = e -> ( ( w = <. d , z >. /\ ( ( ( A ^o X ) .o d ) +o z ) = B ) <-> ( w = <. d , e >. /\ ( ( ( A ^o X ) .o d ) +o e ) = B ) ) )
194 188 193 cbvrex2vw 
 |-  ( E. y e. On E. z e. ( A ^o X ) ( w = <. y , z >. /\ ( ( ( A ^o X ) .o y ) +o z ) = B ) <-> E. d e. On E. e e. ( A ^o X ) ( w = <. d , e >. /\ ( ( ( A ^o X ) .o d ) +o e ) = B ) )
195 eqeq1 
 |-  ( w = a -> ( w = <. d , e >. <-> a = <. d , e >. ) )
196 195 anbi1d 
 |-  ( w = a -> ( ( w = <. d , e >. /\ ( ( ( A ^o X ) .o d ) +o e ) = B ) <-> ( a = <. d , e >. /\ ( ( ( A ^o X ) .o d ) +o e ) = B ) ) )
197 196 2rexbidv 
 |-  ( w = a -> ( E. d e. On E. e e. ( A ^o X ) ( w = <. d , e >. /\ ( ( ( A ^o X ) .o d ) +o e ) = B ) <-> E. d e. On E. e e. ( A ^o X ) ( a = <. d , e >. /\ ( ( ( A ^o X ) .o d ) +o e ) = B ) ) )
198 194 197 bitrid 
 |-  ( w = a -> ( E. y e. On E. z e. ( A ^o X ) ( w = <. y , z >. /\ ( ( ( A ^o X ) .o y ) +o z ) = B ) <-> E. d e. On E. e e. ( A ^o X ) ( a = <. d , e >. /\ ( ( ( A ^o X ) .o d ) +o e ) = B ) ) )
199 198 cbviotavw 
 |-  ( iota w E. y e. On E. z e. ( A ^o X ) ( w = <. y , z >. /\ ( ( ( A ^o X ) .o y ) +o z ) = B ) ) = ( iota a E. d e. On E. e e. ( A ^o X ) ( a = <. d , e >. /\ ( ( ( A ^o X ) .o d ) +o e ) = B ) )
200 2 199 eqtri 
 |-  P = ( iota a E. d e. On E. e e. ( A ^o X ) ( a = <. d , e >. /\ ( ( ( A ^o X ) .o d ) +o e ) = B ) )
201 oveq2 
 |-  ( d = D -> ( ( A ^o X ) .o d ) = ( ( A ^o X ) .o D ) )
202 201 oveq1d 
 |-  ( d = D -> ( ( ( A ^o X ) .o d ) +o e ) = ( ( ( A ^o X ) .o D ) +o e ) )
203 202 eqeq1d 
 |-  ( d = D -> ( ( ( ( A ^o X ) .o d ) +o e ) = B <-> ( ( ( A ^o X ) .o D ) +o e ) = B ) )
204 oveq2 
 |-  ( e = E -> ( ( ( A ^o X ) .o D ) +o e ) = ( ( ( A ^o X ) .o D ) +o E ) )
205 204 eqeq1d 
 |-  ( e = E -> ( ( ( ( A ^o X ) .o D ) +o e ) = B <-> ( ( ( A ^o X ) .o D ) +o E ) = B ) )
206 200 3 4 203 205 opiota 
 |-  ( E! a E. d e. On E. e e. ( A ^o X ) ( a = <. d , e >. /\ ( ( ( A ^o X ) .o d ) +o e ) = B ) -> ( ( D e. On /\ E e. ( A ^o X ) /\ ( ( ( A ^o X ) .o D ) +o E ) = B ) <-> ( D = Y /\ E = Z ) ) )
207 182 206 syl 
 |-  ( ( ( A ^o X ) e. On /\ B e. On /\ ( A ^o X ) =/= (/) ) -> ( ( D e. On /\ E e. ( A ^o X ) /\ ( ( ( A ^o X ) .o D ) +o E ) = B ) <-> ( D = Y /\ E = Z ) ) )
208 178 143 181 207 syl3anc 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( ( D e. On /\ E e. ( A ^o X ) /\ ( ( ( A ^o X ) .o D ) +o E ) = B ) <-> ( D = Y /\ E = Z ) ) )
209 177 208 sylan9bbr 
 |-  ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ C = X ) -> ( ( D e. On /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) <-> ( D = Y /\ E = Z ) ) )
210 209 pm5.32da 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( ( C = X /\ ( D e. On /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) ) <-> ( C = X /\ ( D = Y /\ E = Z ) ) ) )
211 169 210 bitrd 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( ( ( C e. On /\ D e. ( A \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) <-> ( C = X /\ ( D = Y /\ E = Z ) ) ) )
212 3an4anass 
 |-  ( ( ( C e. On /\ D e. ( A \ 1o ) /\ E e. ( A ^o C ) ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) <-> ( ( C e. On /\ D e. ( A \ 1o ) ) /\ ( E e. ( A ^o C ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) ) )
213 3anass 
 |-  ( ( C = X /\ D = Y /\ E = Z ) <-> ( C = X /\ ( D = Y /\ E = Z ) ) )
214 211 212 213 3bitr4g 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( ( ( C e. On /\ D e. ( A \ 1o ) /\ E e. ( A ^o C ) ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) <-> ( C = X /\ D = Y /\ E = Z ) ) )