Metamath Proof Explorer

Theorem oeeu

Description: The division algorithm for ordinal exponentiation. (Contributed by Mario Carneiro, 25-May-2015)

Ref Expression
Assertion oeeu 
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> E! w E. x e. On E. y e. ( A \ 1o ) E. z e. ( A ^o x ) ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. |^| { a e. On | B e. ( A ^o a ) } = U. |^| { a e. On | B e. ( A ^o a ) }
2 1 oeeulem 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( U. |^| { a e. On | B e. ( A ^o a ) } e. On /\ ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) C_ B /\ B e. ( A ^o suc U. |^| { a e. On | B e. ( A ^o a ) } ) ) )
3 2 simp1d 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> U. |^| { a e. On | B e. ( A ^o a ) } e. On )
4 fvexd 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( 1st ` ( iota d E. b e. On E. c e. ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) ( d = <. b , c >. /\ ( ( ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) .o b ) +o c ) = B ) ) ) e. _V )
5 fvexd 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( 2nd ` ( iota d E. b e. On E. c e. ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) ( d = <. b , c >. /\ ( ( ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) .o b ) +o c ) = B ) ) ) e. _V )
6 eqid 
 |-  ( iota d E. b e. On E. c e. ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) ( d = <. b , c >. /\ ( ( ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) .o b ) +o c ) = B ) ) = ( iota d E. b e. On E. c e. ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) ( d = <. b , c >. /\ ( ( ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) .o b ) +o c ) = B ) )
7 eqid 
 |-  ( 1st ` ( iota d E. b e. On E. c e. ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) ( d = <. b , c >. /\ ( ( ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) .o b ) +o c ) = B ) ) ) = ( 1st ` ( iota d E. b e. On E. c e. ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) ( d = <. b , c >. /\ ( ( ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) .o b ) +o c ) = B ) ) )
8 eqid 
 |-  ( 2nd ` ( iota d E. b e. On E. c e. ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) ( d = <. b , c >. /\ ( ( ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) .o b ) +o c ) = B ) ) ) = ( 2nd ` ( iota d E. b e. On E. c e. ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) ( d = <. b , c >. /\ ( ( ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) .o b ) +o c ) = B ) ) )
9 1 6 7 8 oeeui 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( ( ( x e. On /\ y e. ( A \ 1o ) /\ z e. ( A ^o x ) ) /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) <-> ( x = U. |^| { a e. On | B e. ( A ^o a ) } /\ y = ( 1st ` ( iota d E. b e. On E. c e. ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) ( d = <. b , c >. /\ ( ( ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) .o b ) +o c ) = B ) ) ) /\ z = ( 2nd ` ( iota d E. b e. On E. c e. ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) ( d = <. b , c >. /\ ( ( ( A ^o U. |^| { a e. On | B e. ( A ^o a ) } ) .o b ) +o c ) = B ) ) ) ) ) )
10 3 4 5 9 euotd 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> E! w E. x E. y E. z ( w = <. x , y , z >. /\ ( ( x e. On /\ y e. ( A \ 1o ) /\ z e. ( A ^o x ) ) /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) )
11 df-3an 
 |-  ( ( x e. On /\ y e. ( A \ 1o ) /\ z e. ( A ^o x ) ) <-> ( ( x e. On /\ y e. ( A \ 1o ) ) /\ z e. ( A ^o x ) ) )
12 11 biancomi 
 |-  ( ( x e. On /\ y e. ( A \ 1o ) /\ z e. ( A ^o x ) ) <-> ( z e. ( A ^o x ) /\ ( x e. On /\ y e. ( A \ 1o ) ) ) )
13 12 anbi1i 
 |-  ( ( ( x e. On /\ y e. ( A \ 1o ) /\ z e. ( A ^o x ) ) /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) <-> ( ( z e. ( A ^o x ) /\ ( x e. On /\ y e. ( A \ 1o ) ) ) /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) )
14 13 anbi2i 
 |-  ( ( w = <. x , y , z >. /\ ( ( x e. On /\ y e. ( A \ 1o ) /\ z e. ( A ^o x ) ) /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) <-> ( w = <. x , y , z >. /\ ( ( z e. ( A ^o x ) /\ ( x e. On /\ y e. ( A \ 1o ) ) ) /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) )
15 an12 
 |-  ( ( w = <. x , y , z >. /\ ( ( z e. ( A ^o x ) /\ ( x e. On /\ y e. ( A \ 1o ) ) ) /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) <-> ( ( z e. ( A ^o x ) /\ ( x e. On /\ y e. ( A \ 1o ) ) ) /\ ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) )
16 anass 
 |-  ( ( ( z e. ( A ^o x ) /\ ( x e. On /\ y e. ( A \ 1o ) ) ) /\ ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) <-> ( z e. ( A ^o x ) /\ ( ( x e. On /\ y e. ( A \ 1o ) ) /\ ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) ) )
17 14 15 16 3bitri 
 |-  ( ( w = <. x , y , z >. /\ ( ( x e. On /\ y e. ( A \ 1o ) /\ z e. ( A ^o x ) ) /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) <-> ( z e. ( A ^o x ) /\ ( ( x e. On /\ y e. ( A \ 1o ) ) /\ ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) ) )
18 17 exbii 
 |-  ( E. z ( w = <. x , y , z >. /\ ( ( x e. On /\ y e. ( A \ 1o ) /\ z e. ( A ^o x ) ) /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) <-> E. z ( z e. ( A ^o x ) /\ ( ( x e. On /\ y e. ( A \ 1o ) ) /\ ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) ) )
19 df-rex 
 |-  ( E. z e. ( A ^o x ) ( ( x e. On /\ y e. ( A \ 1o ) ) /\ ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) <-> E. z ( z e. ( A ^o x ) /\ ( ( x e. On /\ y e. ( A \ 1o ) ) /\ ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) ) )
20 r19.42v 
 |-  ( E. z e. ( A ^o x ) ( ( x e. On /\ y e. ( A \ 1o ) ) /\ ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) <-> ( ( x e. On /\ y e. ( A \ 1o ) ) /\ E. z e. ( A ^o x ) ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) )
21 18 19 20 3bitr2i 
 |-  ( E. z ( w = <. x , y , z >. /\ ( ( x e. On /\ y e. ( A \ 1o ) /\ z e. ( A ^o x ) ) /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) <-> ( ( x e. On /\ y e. ( A \ 1o ) ) /\ E. z e. ( A ^o x ) ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) )
22 21 2exbii 
 |-  ( E. x E. y E. z ( w = <. x , y , z >. /\ ( ( x e. On /\ y e. ( A \ 1o ) /\ z e. ( A ^o x ) ) /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) <-> E. x E. y ( ( x e. On /\ y e. ( A \ 1o ) ) /\ E. z e. ( A ^o x ) ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) )
23 r2ex 
 |-  ( E. x e. On E. y e. ( A \ 1o ) E. z e. ( A ^o x ) ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) <-> E. x E. y ( ( x e. On /\ y e. ( A \ 1o ) ) /\ E. z e. ( A ^o x ) ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) )
24 22 23 bitr4i 
 |-  ( E. x E. y E. z ( w = <. x , y , z >. /\ ( ( x e. On /\ y e. ( A \ 1o ) /\ z e. ( A ^o x ) ) /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) <-> E. x e. On E. y e. ( A \ 1o ) E. z e. ( A ^o x ) ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) )
25 24 eubii 
 |-  ( E! w E. x E. y E. z ( w = <. x , y , z >. /\ ( ( x e. On /\ y e. ( A \ 1o ) /\ z e. ( A ^o x ) ) /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) ) <-> E! w E. x e. On E. y e. ( A \ 1o ) E. z e. ( A ^o x ) ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) )
26 10 25 sylib 
 |-  ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> E! w E. x e. On E. y e. ( A \ 1o ) E. z e. ( A ^o x ) ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) )