Metamath Proof Explorer

Theorem omeu

Description: The division algorithm for ordinal multiplication. (Contributed by Mario Carneiro, 28-Feb-2013)

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

Proof

Step Hyp Ref Expression
1 omeulem1 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> E. x e. On E. y e. A ( ( A .o x ) +o y ) = B )
2 opex 
 |-  <. x , y >. e. _V
3 2 isseti 
 |-  E. z z = <. x , y >.
4 19.41v 
 |-  ( E. z ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> ( E. z z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) )
5 3 4 mpbiran 
 |-  ( E. z ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> ( ( A .o x ) +o y ) = B )
6 5 rexbii 
 |-  ( E. y e. A E. z ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> E. y e. A ( ( A .o x ) +o y ) = B )
7 rexcom4 
 |-  ( E. y e. A E. z ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> E. z E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) )
8 6 7 bitr3i 
 |-  ( E. y e. A ( ( A .o x ) +o y ) = B <-> E. z E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) )
9 8 rexbii 
 |-  ( E. x e. On E. y e. A ( ( A .o x ) +o y ) = B <-> E. x e. On E. z E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) )
10 rexcom4 
 |-  ( E. x e. On E. z E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> E. z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) )
11 9 10 bitri 
 |-  ( E. x e. On E. y e. A ( ( A .o x ) +o y ) = B <-> E. z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) )
12 1 11 sylib 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> E. z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) )
13 simp2rl 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> z = <. x , y >. )
14 simp3rl 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> t = <. r , s >. )
15 simp2rr 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> ( ( A .o x ) +o y ) = B )
16 simp3rr 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> ( ( A .o r ) +o s ) = B )
17 15 16 eqtr4d 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> ( ( A .o x ) +o y ) = ( ( A .o r ) +o s ) )
18 simp11 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> A e. On )
19 simp13 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> A =/= (/) )
20 simp2ll 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> x e. On )
21 simp2lr 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> y e. A )
22 simp3ll 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> r e. On )
23 simp3lr 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> s e. A )
24 omopth2 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( x e. On /\ y e. A ) /\ ( r e. On /\ s e. A ) ) -> ( ( ( A .o x ) +o y ) = ( ( A .o r ) +o s ) <-> ( x = r /\ y = s ) ) )
25 18 19 20 21 22 23 24 syl222anc 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> ( ( ( A .o x ) +o y ) = ( ( A .o r ) +o s ) <-> ( x = r /\ y = s ) ) )
26 17 25 mpbid 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> ( x = r /\ y = s ) )
27 opeq12 
 |-  ( ( x = r /\ y = s ) -> <. x , y >. = <. r , s >. )
28 26 27 syl 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> <. x , y >. = <. r , s >. )
29 14 28 eqtr4d 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> t = <. x , y >. )
30 13 29 eqtr4d 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> z = t )
31 30 3expia 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) ) -> ( ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) -> z = t ) )
32 31 exp4b 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> ( ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) -> ( ( r e. On /\ s e. A ) -> ( ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) -> z = t ) ) ) )
33 32 expd 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> ( ( x e. On /\ y e. A ) -> ( ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) -> ( ( r e. On /\ s e. A ) -> ( ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) -> z = t ) ) ) ) )
34 33 rexlimdvv 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> ( E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) -> ( ( r e. On /\ s e. A ) -> ( ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) -> z = t ) ) ) )
35 34 imp 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) -> ( ( r e. On /\ s e. A ) -> ( ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) -> z = t ) ) )
36 35 rexlimdvv 
 |-  ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) -> ( E. r e. On E. s e. A ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) -> z = t ) )
37 36 expimpd 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> ( ( E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) /\ E. r e. On E. s e. A ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) -> z = t ) )
38 37 alrimivv 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> A. z A. t ( ( E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) /\ E. r e. On E. s e. A ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) -> z = t ) )
39 opeq1 
 |-  ( x = r -> <. x , y >. = <. r , y >. )
40 39 eqeq2d 
 |-  ( x = r -> ( z = <. x , y >. <-> z = <. r , y >. ) )
41 oveq2 
 |-  ( x = r -> ( A .o x ) = ( A .o r ) )
42 41 oveq1d 
 |-  ( x = r -> ( ( A .o x ) +o y ) = ( ( A .o r ) +o y ) )
43 42 eqeq1d 
 |-  ( x = r -> ( ( ( A .o x ) +o y ) = B <-> ( ( A .o r ) +o y ) = B ) )
44 40 43 anbi12d 
 |-  ( x = r -> ( ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> ( z = <. r , y >. /\ ( ( A .o r ) +o y ) = B ) ) )
45 opeq2 
 |-  ( y = s -> <. r , y >. = <. r , s >. )
46 45 eqeq2d 
 |-  ( y = s -> ( z = <. r , y >. <-> z = <. r , s >. ) )
47 oveq2 
 |-  ( y = s -> ( ( A .o r ) +o y ) = ( ( A .o r ) +o s ) )
48 47 eqeq1d 
 |-  ( y = s -> ( ( ( A .o r ) +o y ) = B <-> ( ( A .o r ) +o s ) = B ) )
49 46 48 anbi12d 
 |-  ( y = s -> ( ( z = <. r , y >. /\ ( ( A .o r ) +o y ) = B ) <-> ( z = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) )
50 44 49 cbvrex2vw 
 |-  ( E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> E. r e. On E. s e. A ( z = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) )
51 eqeq1 
 |-  ( z = t -> ( z = <. r , s >. <-> t = <. r , s >. ) )
52 51 anbi1d 
 |-  ( z = t -> ( ( z = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) <-> ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) )
53 52 2rexbidv 
 |-  ( z = t -> ( E. r e. On E. s e. A ( z = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) <-> E. r e. On E. s e. A ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) )
54 50 53 syl5bb 
 |-  ( z = t -> ( E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> E. r e. On E. s e. A ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) )
55 54 eu4 
 |-  ( E! z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> ( E. z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) /\ A. z A. t ( ( E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) /\ E. r e. On E. s e. A ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) -> z = t ) ) )
56 12 38 55 sylanbrc 
 |-  ( ( A e. On /\ B e. On /\ A =/= (/) ) -> E! z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) )