MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oeeui Structured version   Visualization version   Unicode version
Theorem oeeui 7682
Description: The division algorithm for ordinal exponentiation. (This version of oeeu 7683 gives an explicit expression for the unique solution of the equation, in terms of the solution P to omeu 7665.) (Contributed by Mario Carneiro, 25-May-2015.)
Hypotheses
Ref Expression
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
Ref Expression
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 ) ) )
Distinct variable groups:   x, w, y, z, A   w, B, x, y, z   w, X, y, z
Allowed substitution hints:   C( x, y, z, w)   D( x, y, z, w)   P( x, y, z, w)   E( x, y, z, w)   X( x)   Y( x, y, z, w)   Z( x, y, z, w)
Proof of Theorem oeeui
Dummy variables a d e are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldifi 3732 . . . . . . . . . . . . . . . . . 18 |- ( A e. ( On \ 2o ) -> A e. On )
21adantr 481 . . . . . . . . . . . . . . . . 17 |- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> A e. On )
32ad2antrr 762 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
4 simprl 794 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
5 oecl 7617 . . . . . . . . . . . . . . . 16 |- ( ( A e. On /\ C e. On ) -> ( A ^o C ) e. On )
63, 4, 5syl2anc 693 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
7 om1 7622 . . . . . . . . . . . . . . 15 |- ( ( A ^o C ) e. On -> ( ( A ^o C ) .o 1o ) = ( A ^o C ) )
86, 7syl 17 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
9 df1o2 7572 . . . . . . . . . . . . . . . 16 |- 1o = { (/) }
10 dif1o 7580 . . . . . . . . . . . . . . . . . . . 20 |- ( D e. ( A \ 1o ) <-> ( D e. A /\ D =/= (/) ) )
1110simprbi 480 . . . . . . . . . . . . . . . . . . 19 |- ( D e. ( A \ 1o ) -> D =/= (/) )
1211ad2antll 765 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 =/= (/) )
13 eldifi 3732 . . . . . . . . . . . . . . . . . . . . 21 |- ( D e. ( A \ 1o ) -> D e. A )
1413ad2antll 765 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 )
15 onelon 5748 . . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. On /\ D e. A ) -> D e. On )
163, 14, 15syl2anc 693 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 )
17 on0eln0 5780 . . . . . . . . . . . . . . . . . . 19 |- ( D e. On -> ( (/) e. D <-> D =/= (/) ) )
1816, 17syl 17 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 =/= (/) ) )
1912, 18mpbird 247 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
2019snssd 4340 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
219, 20syl5eqss 3649 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
22 1on 7567 . . . . . . . . . . . . . . . . 17 |- 1o e. On
2322a1i 11 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
24 omwordi 7651 . . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) )
2523, 16, 6, 24syl3anc 1326 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) )
2621, 25mpd 15 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
278, 26eqsstr3d 3640 . . . . . . . . . . . . 13 |- ( ( ( ( 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 ) )
28 omcl 7616 . . . . . . . . . . . . . . . 16 |- ( ( ( A ^o C ) e. On /\ D e. On ) -> ( ( A ^o C ) .o D ) e. On )
296, 16, 28syl2anc 693 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
30 simplrl 800 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) )
31 onelon 5748 . . . . . . . . . . . . . . . 16 |- ( ( ( A ^o C ) e. On /\ E e. ( A ^o C ) ) -> E e. On )
326, 30, 31syl2anc 693 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
33 oaword1 7632 . . . . . . . . . . . . . . 15 |- ( ( ( ( A ^o C ) .o D ) e. On /\ E e. On ) -> ( ( A ^o C ) .o D ) C_ ( ( ( A ^o C ) .o D ) +o E ) )
3429, 32, 33syl2anc 693 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
35 simplrr 801 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 )
3634, 35sseqtrd 3641 . . . . . . . . . . . . 13 |- ( ( ( ( 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 )
3727, 36sstrd 3613 . . . . . . . . . . . 12 |- ( ( ( ( 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 )
38 oeeu.1 . . . . . . . . . . . . . . 15 |- X = U. |^| { x e. On | B e. ( A ^o x ) }
3938oeeulem 7681 . . . . . . . . . . . . . 14 |- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( X e. On /\ ( A ^o X ) C_ B /\ B e. ( A ^o suc X ) ) )
4039simp3d 1075 . . . . . . . . . . . . 13 |- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> B e. ( A ^o suc X ) )
4140ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
4239simp1d 1073 . . . . . . . . . . . . . . . 16 |- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> X e. On )
4342ad2antrr 762 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
44 suceloni 7013 . . . . . . . . . . . . . . 15 |- ( X e. On -> suc X e. On )
4543, 44syl 17 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 )
46 oecl 7617 . . . . . . . . . . . . . 14 |- ( ( A e. On /\ suc X e. On ) -> ( A ^o suc X ) e. On )
473, 45, 46syl2anc 693 . . . . . . . . . . . . 13 |- ( ( ( ( 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 )
48 ontr2 5772 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
496, 47, 48syl2anc 693 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) )
5037, 41, 49mp2and 715 . . . . . . . . . . 11 |- ( ( ( ( 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 ) )
51 simplll 798 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
52 oeord 7668 . . . . . . . . . . . 12 |- ( ( C e. On /\ suc X e. On /\ A e. ( On \ 2o ) ) -> ( C e. suc X <-> ( A ^o C ) e. ( A ^o suc X ) ) )
534, 45, 51, 52syl3anc 1326 . . . . . . . . . . 11 |- ( ( ( ( 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 ) ) )
5450, 53mpbird 247 . . . . . . . . . 10 |- ( ( ( ( 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 )
55 onsssuc 5813 . . . . . . . . . . 11 |- ( ( C e. On /\ X e. On ) -> ( C C_ X <-> C e. suc X ) )
564, 43, 55syl2anc 693 . . . . . . . . . 10 |- ( ( ( ( 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 ) )
5754, 56mpbird 247 . . . . . . . . 9 |- ( ( ( ( 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 )
5839simp2d 1074 . . . . . . . . . . . . 13 |- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( A ^o X ) C_ B )
5958ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ( 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 )
60 eloni 5733 . . . . . . . . . . . . . . . . 17 |- ( A e. On -> Ord A )
613, 60syl 17 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
62 ordsucss 7018 . . . . . . . . . . . . . . . 16 |- ( Ord A -> ( D e. A -> suc D C_ A ) )
6361, 14, 62sylc 65 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
64 suceloni 7013 . . . . . . . . . . . . . . . . 17 |- ( D e. On -> suc D e. On )
6516, 64syl 17 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
66 dif20el 7585 . . . . . . . . . . . . . . . . . 18 |- ( A e. ( On \ 2o ) -> (/) e. A )
6751, 66syl 17 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
68 oen0 7666 . . . . . . . . . . . . . . . . 17 |- ( ( ( A e. On /\ C e. On ) /\ (/) e. A ) -> (/) e. ( A ^o C ) )
693, 4, 67, 68syl21anc 1325 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) )
70 omword 7650 . . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) ) )
7165, 3, 6, 69, 70syl31anc 1329 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) )
7263, 71mpbid 222 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
73 oaord 7627 . . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) ) )
7432, 6, 29, 73syl3anc 1326 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 ) ) ) )
7530, 74mpbid 222 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) ) )
7635, 75eqeltrrd 2702 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) )
77 odi 7659 . . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) )
786, 16, 23, 77syl3anc 1326 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) ) )
79 oa1suc 7611 . . . . . . . . . . . . . . . . . 18 |- ( D e. On -> ( D +o 1o ) = suc D )
8016, 79syl 17 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
8180oveq2d 6666 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) )
828oveq2d 6666 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) ) )
8378, 81, 823eqtr3d 2664 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) )
8476, 83eleqtrrd 2704 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
8572, 84sseldd 3604 . . . . . . . . . . . . 13 |- ( ( ( ( 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 ) )
86 oesuc 7607 . . . . . . . . . . . . . 14 |- ( ( A e. On /\ C e. On ) -> ( A ^o suc C ) = ( ( A ^o C ) .o A ) )
873, 4, 86syl2anc 693 . . . . . . . . . . . . 13 |- ( ( ( ( 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 ) )
8885, 87eleqtrrd 2704 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
89 oecl 7617 . . . . . . . . . . . . . 14 |- ( ( A e. On /\ X e. On ) -> ( A ^o X ) e. On )
903, 43, 89syl2anc 693 . . . . . . . . . . . . 13 |- ( ( ( ( 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 )
91 suceloni 7013 . . . . . . . . . . . . . . 15 |- ( C e. On -> suc C e. On )
9291ad2antrl 764 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 )
93 oecl 7617 . . . . . . . . . . . . . 14 |- ( ( A e. On /\ suc C e. On ) -> ( A ^o suc C ) e. On )
943, 92, 93syl2anc 693 . . . . . . . . . . . . 13 |- ( ( ( ( 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 )
95 ontr2 5772 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
9690, 94, 95syl2anc 693 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) )
9759, 88, 96mp2and 715 . . . . . . . . . . 11 |- ( ( ( ( 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 ) )
98 oeord 7668 . . . . . . . . . . . 12 |- ( ( X e. On /\ suc C e. On /\ A e. ( On \ 2o ) ) -> ( X e. suc C <-> ( A ^o X ) e. ( A ^o suc C ) ) )
9943, 92, 51, 98syl3anc 1326 . . . . . . . . . . 11 |- ( ( ( ( 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 ) ) )
10097, 99mpbird 247 . . . . . . . . . 10 |- ( ( ( ( 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 )
101 onsssuc 5813 . . . . . . . . . . 11 |- ( ( X e. On /\ C e. On ) -> ( X C_ C <-> X e. suc C ) )
10243, 4, 101syl2anc 693 . . . . . . . . . 10 |- ( ( ( ( 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 ) )
103100, 102mpbird 247 . . . . . . . . 9 |- ( ( ( ( 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 )
10457, 103eqssd 3620 . . . . . . . 8 |- ( ( ( ( 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 )
105104, 16jca 554 . . . . . . 7 |- ( ( ( ( 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 ) )
106 simprl 794 . . . . . . . . 9 |- ( ( ( ( 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 )
10742ad2antrr 762 . . . . . . . . 9 |- ( ( ( ( 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 )
108106, 107eqeltrd 2701 . . . . . . . 8 |- ( ( ( ( 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 )
1092ad2antrr 762 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
110109, 108, 5syl2anc 693 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 )
111 simprr 796 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 )
112110, 111, 28syl2anc 693 . . . . . . . . . . . . 13 |- ( ( ( ( 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 )
113 simplrl 800 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
114110, 113, 31syl2anc 693 . . . . . . . . . . . . 13 |- ( ( ( ( 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 )
115112, 114, 33syl2anc 693 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
116 simplrr 801 . . . . . . . . . . . 12 |- ( ( ( ( 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 )
117115, 116sseqtrd 3641 . . . . . . . . . . 11 |- ( ( ( ( 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 )
11840ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
119 suceq 5790 . . . . . . . . . . . . . . 15 |- ( C = X -> suc C = suc X )
120119ad2antrl 764 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 )
121120oveq2d 6666 . . . . . . . . . . . . 13 |- ( ( ( ( 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 ) )
122109, 108, 86syl2anc 693 . . . . . . . . . . . . 13 |- ( ( ( ( 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 ) )
123121, 122eqtr3d 2658 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
124118, 123eleqtrd 2703 . . . . . . . . . . 11 |- ( ( ( ( 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 ) )
125 omcl 7616 . . . . . . . . . . . . 13 |- ( ( ( A ^o C ) e. On /\ A e. On ) -> ( ( A ^o C ) .o A ) e. On )
126110, 109, 125syl2anc 693 . . . . . . . . . . . 12 |- ( ( ( ( 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 )
127 ontr2 5772 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) )
128112, 126, 127syl2anc 693 . . . . . . . . . . 11 |- ( ( ( ( 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 ) ) )
129117, 124, 128mp2and 715 . . . . . . . . . 10 |- ( ( ( ( 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 ) )
13066adantr 481 . . . . . . . . . . . . 13 |- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> (/) e. A )
131130ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ( 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 )
132109, 108, 131, 68syl21anc 1325 . . . . . . . . . . 11 |- ( ( ( ( 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 ) )
133 omord2 7647 . . . . . . . . . . 11 |- ( ( ( 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 ) ) )
134111, 109, 110, 132, 133syl31anc 1329 . . . . . . . . . 10 |- ( ( ( ( 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 ) ) )
135129, 134mpbird 247 . . . . . . . . 9 |- ( ( ( ( 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 )
136106oveq2d 6666 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
13758ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ( 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 )
138136, 137eqsstrd 3639 . . . . . . . . . . 11 |- ( ( ( ( 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 )
139 eldifi 3732 . . . . . . . . . . . . . 14 |- ( B e. ( On \ 1o ) -> B e. On )
140139adantl 482 . . . . . . . . . . . . 13 |- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> B e. On )
141140ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ( 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 )
142 ontri1 5757 . . . . . . . . . . . 12 |- ( ( ( A ^o C ) e. On /\ B e. On ) -> ( ( A ^o C ) C_ B <-> -. B e. ( A ^o C ) ) )
143110, 141, 142syl2anc 693 . . . . . . . . . . 11 |- ( ( ( ( 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 ) ) )
144138, 143mpbid 222 . . . . . . . . . 10 |- ( ( ( ( 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 ) )
145 om0 7597 . . . . . . . . . . . . . . . . 17 |- ( ( A ^o C ) e. On -> ( ( A ^o C ) .o (/) ) = (/) )
146110, 145syl 17 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 (/) ) = (/) )
147146oveq1d 6665 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) )
148 oa0r 7618 . . . . . . . . . . . . . . . 16 |- ( E e. On -> ( (/) +o E ) = E )
149114, 148syl 17 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
150147, 149eqtrd 2656 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 )
151150, 113eqeltrd 2701 . . . . . . . . . . . . 13 |- ( ( ( ( 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 ) )
152 oveq2 6658 . . . . . . . . . . . . . . 15 |- ( D = (/) -> ( ( A ^o C ) .o D ) = ( ( A ^o C ) .o (/) ) )
153152oveq1d 6665 . . . . . . . . . . . . . 14 |- ( D = (/) -> ( ( ( A ^o C ) .o D ) +o E ) = ( ( ( A ^o C ) .o (/) ) +o E ) )
154153eleq1d 2686 . . . . . . . . . . . . 13 |- ( D = (/) -> ( ( ( ( A ^o C ) .o D ) +o E ) e. ( A ^o C ) <-> ( ( ( A ^o C ) .o (/) ) +o E ) e. ( A ^o C ) ) )
155151, 154syl5ibrcom 237 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) )
156116eleq1d 2686 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) )
157155, 156sylibd 229 . . . . . . . . . . 11 |- ( ( ( ( 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 ) ) )
158157necon3bd 2808 . . . . . . . . . 10 |- ( ( ( ( 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 =/= (/) ) )
159144, 158mpd 15 . . . . . . . . 9 |- ( ( ( ( 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 =/= (/) )
160135, 159, 10sylanbrc 698 . . . . . . . 8 |- ( ( ( ( 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 ) )
161108, 160jca 554 . . . . . . 7 |- ( ( ( ( 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 ) ) )
162105, 161impbida 877 . . . . . 6 |- ( ( ( 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 ) ) )
163162ex 450 . . . . 5 |- ( ( 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 ) ) ) )
164163pm5.32rd 672 . . . 4 |- ( ( 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 ) ) ) )
165 anass 681 . . . 4 |- ( ( ( 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 ) ) ) )
166164, 165syl6bb 276 . . 3 |- ( ( 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 ) ) ) ) )
167 3anass 1042 . . . . . 6 |- ( ( 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 ) ) )
168 oveq2 6658 . . . . . . . 8 |- ( C = X -> ( A ^o C ) = ( A ^o X ) )
169168eleq2d 2687 . . . . . . 7 |- ( C = X -> ( E e. ( A ^o C ) <-> E e. ( A ^o X ) ) )
170168oveq1d 6665 . . . . . . . . 9 |- ( C = X -> ( ( A ^o C ) .o D ) = ( ( A ^o X ) .o D ) )
171170oveq1d 6665 . . . . . . . 8 |- ( C = X -> ( ( ( A ^o C ) .o D ) +o E ) = ( ( ( A ^o X ) .o D ) +o E ) )
172171eqeq1d 2624 . . . . . . 7 |- ( C = X -> ( ( ( ( A ^o C ) .o D ) +o E ) = B <-> ( ( ( A ^o X ) .o D ) +o E ) = B ) )
173169, 1723anbi23d 1402 . . . . . 6 |- ( 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 ) ) )
174167, 173syl5bbr 274 . . . . 5 |- ( 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 ) ) )
1752, 42, 89syl2anc 693 . . . . . 6 |- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( A ^o X ) e. On )
176 oen0 7666 . . . . . . . 8 |- ( ( ( A e. On /\ X e. On ) /\ (/) e. A ) -> (/) e. ( A ^o X ) )
1772, 42, 130, 176syl21anc 1325 . . . . . . 7 |- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> (/) e. ( A ^o X ) )
178 ne0i 3921 . . . . . . 7 |- ( (/) e. ( A ^o X ) -> ( A ^o X ) =/= (/) )
179177, 178syl 17 . . . . . 6 |- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( A ^o X ) =/= (/) )
180 omeu 7665 . . . . . . 7 |- ( ( ( 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 ) )
181 oeeu.2 . . . . . . . . 9 |- P = ( iota w E. y e. On E. z e. ( A ^o X ) ( w = <. y , z >. /\ ( ( ( A ^o X ) .o y ) +o z ) = B ) )
182 opeq1 4402 . . . . . . . . . . . . . 14 |- ( y = d -> <. y , z >. = <. d , z >. )
183182eqeq2d 2632 . . . . . . . . . . . . 13 |- ( y = d -> ( w = <. y , z >. <-> w = <. d , z >. ) )
184 oveq2 6658 . . . . . . . . . . . . . . 15 |- ( y = d -> ( ( A ^o X ) .o y ) = ( ( A ^o X ) .o d ) )
185184oveq1d 6665 . . . . . . . . . . . . . 14 |- ( y = d -> ( ( ( A ^o X ) .o y ) +o z ) = ( ( ( A ^o X ) .o d ) +o z ) )
186185eqeq1d 2624 . . . . . . . . . . . . 13 |- ( y = d -> ( ( ( ( A ^o X ) .o y ) +o z ) = B <-> ( ( ( A ^o X ) .o d ) +o z ) = B ) )
187183, 186anbi12d 747 . . . . . . . . . . . 12 |- ( y = d -> ( ( w = <. y , z >. /\ ( ( ( A ^o X ) .o y ) +o z ) = B ) <-> ( w = <. d , z >. /\ ( ( ( A ^o X ) .o d ) +o z ) = B ) ) )
188 opeq2 4403 . . . . . . . . . . . . . 14 |- ( z = e -> <. d , z >. = <. d , e >. )
189188eqeq2d 2632 . . . . . . . . . . . . 13 |- ( z = e -> ( w = <. d , z >. <-> w = <. d , e >. ) )
190 oveq2 6658 . . . . . . . . . . . . . 14 |- ( z = e -> ( ( ( A ^o X ) .o d ) +o z ) = ( ( ( A ^o X ) .o d ) +o e ) )
191190eqeq1d 2624 . . . . . . . . . . . . 13 |- ( z = e -> ( ( ( ( A ^o X ) .o d ) +o z ) = B <-> ( ( ( A ^o X ) .o d ) +o e ) = B ) )
192189, 191anbi12d 747 . . . . . . . . . . . 12 |- ( z = e -> ( ( w = <. d , z >. /\ ( ( ( A ^o X ) .o d ) +o z ) = B ) <-> ( w = <. d , e >. /\ ( ( ( A ^o X ) .o d ) +o e ) = B ) ) )
193187, 192cbvrex2v 3180 . . . . . . . . . . 11 |- ( 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 ) )
194 eqeq1 2626 . . . . . . . . . . . . 13 |- ( w = a -> ( w = <. d , e >. <-> a = <. d , e >. ) )
195194anbi1d 741 . . . . . . . . . . . 12 |- ( w = a -> ( ( w = <. d , e >. /\ ( ( ( A ^o X ) .o d ) +o e ) = B ) <-> ( a = <. d , e >. /\ ( ( ( A ^o X ) .o d ) +o e ) = B ) ) )
1961952rexbidv 3057 . . . . . . . . . . 11 |- ( 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 ) ) )
197193, 196syl5bb 272 . . . . . . . . . 10 |- ( 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 ) ) )
198197cbviotav 5857 . . . . . . . . 9 |- ( 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 ) )
199181, 198eqtri 2644 . . . . . . . 8 |- P = ( iota a E. d e. On E. e e. ( A ^o X ) ( a = <. d , e >. /\ ( ( ( A ^o X ) .o d ) +o e ) = B ) )
200 oeeu.3 . . . . . . . 8 |- Y = ( 1st ` P )
201 oeeu.4 . . . . . . . 8 |- Z = ( 2nd ` P )
202 oveq2 6658 . . . . . . . . . 10 |- ( d = D -> ( ( A ^o X ) .o d ) = ( ( A ^o X ) .o D ) )
203202oveq1d 6665 . . . . . . . . 9 |- ( d = D -> ( ( ( A ^o X ) .o d ) +o e ) = ( ( ( A ^o X ) .o D ) +o e ) )
204203eqeq1d 2624 . . . . . . . 8 |- ( d = D -> ( ( ( ( A ^o X ) .o d ) +o e ) = B <-> ( ( ( A ^o X ) .o D ) +o e ) = B ) )
205 oveq2 6658 . . . . . . . . 9 |- ( e = E -> ( ( ( A ^o X ) .o D ) +o e ) = ( ( ( A ^o X ) .o D ) +o E ) )
206205eqeq1d 2624 . . . . . . . 8 |- ( e = E -> ( ( ( ( A ^o X ) .o D ) +o e ) = B <-> ( ( ( A ^o X ) .o D ) +o E ) = B ) )
207199, 200, 201, 204, 206opiota 7229 . . . . . . 7 |- ( 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 ) ) )
208180, 207syl 17 . . . . . 6 |- ( ( ( 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 ) ) )
209175, 140, 179, 208syl3anc 1326 . . . . 5 |- ( ( 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 ) ) )
210174, 209sylan9bbr 737 . . . 4 |- ( ( ( 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 ) ) )
211210pm5.32da 673 . . 3 |- ( ( 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 ) ) ) )
212166, 211bitrd 268 . 2 |- ( ( 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 ) ) ) )
213 3an4anass 1291 . 2 |- ( ( ( 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 ) ) )
214 3anass 1042 . 2 |- ( ( C = X /\ D = Y /\ E = Z ) <-> ( C = X /\ ( D = Y /\ E = Z ) ) )
215212, 213, 2143bitr4g 303 1 |- ( ( 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 ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   E!weu 2470   =/= wne 2794   E.wrex 2913   {crab 2916   \ cdif 3571   C_ wss 3574   (/)c0 3915   {csn 4177   <.cop 4183   U.cuni 4436   |^|cint 4475   Ord word 5722   Oncon0 5723   suc csuc 5725   iotacio 5849   ` cfv 5888  (class class class)co 6650   1stc1st 7166   2ndc2nd 7167   1oc1o 7553   2oc2o 7554   +o coa 7557   .o comu 7558   ^o coe 7559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-omul 7565  df-oexp 7566
This theorem is referenced by:  oeeu  7683  cantnflem3  8588  cantnflem4  8589
  Copyright terms: Public domain W3C validator