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 ) )