Metamath Proof Explorer

Theorem omeueq

Description: The division algorithm for ordinal multiplication ( omeu ) produces a unique quotient and remainder. (Contributed by BTernaryTau, 5-Oct-2026)

Ref Expression
Hypotheses omeueq.1 
|- ( ph -> A e. On )
omeueq.2 
|- ( ph -> A =/= (/) )
omeueq.3 
|- ( ph -> B e. On )
omeueq.4 
|- ( ph -> C e. A )
omeueq.5 
|- ( ph -> D e. On )
omeueq.6 
|- ( ph -> E e. A )
omeueq.7 
|- ( ph -> ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) )
Assertion omeueq 
|- ( ph -> ( B = D /\ C = E ) )

Proof

Step Hyp Ref Expression
1 omeueq.1 
 |-  ( ph -> A e. On )
2 omeueq.2 
 |-  ( ph -> A =/= (/) )
3 omeueq.3 
 |-  ( ph -> B e. On )
4 omeueq.4 
 |-  ( ph -> C e. A )
5 omeueq.5 
 |-  ( ph -> D e. On )
6 omeueq.6 
 |-  ( ph -> E e. A )
7 omeueq.7 
 |-  ( ph -> ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) )
8 omcl 
 |-  ( ( A e. On /\ B e. On ) -> ( A .o B ) e. On )
9 1 3 8 syl2anc 
 |-  ( ph -> ( A .o B ) e. On )
10 onelon 
 |-  ( ( A e. On /\ C e. A ) -> C e. On )
11 1 4 10 syl2anc 
 |-  ( ph -> C e. On )
12 oacl 
 |-  ( ( ( A .o B ) e. On /\ C e. On ) -> ( ( A .o B ) +o C ) e. On )
13 9 11 12 syl2anc 
 |-  ( ph -> ( ( A .o B ) +o C ) e. On )
14 omeu 
 |-  ( ( A e. On /\ ( ( A .o B ) +o C ) e. On /\ A =/= (/) ) -> E! z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) )
15 1 13 2 14 syl3anc 
 |-  ( ph -> E! z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) )
16 eumo 
 |-  ( E! z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) -> E* z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) )
17 15 16 syl 
 |-  ( ph -> E* z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) )
18 opeq1 
 |-  ( x = B -> <. x , y >. = <. B , y >. )
19 18 eqeq2d 
 |-  ( x = B -> ( <. B , C >. = <. x , y >. <-> <. B , C >. = <. B , y >. ) )
20 oveq2 
 |-  ( x = B -> ( A .o x ) = ( A .o B ) )
21 20 oveq1d 
 |-  ( x = B -> ( ( A .o x ) +o y ) = ( ( A .o B ) +o y ) )
22 21 eqeq1d 
 |-  ( x = B -> ( ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) <-> ( ( A .o B ) +o y ) = ( ( A .o B ) +o C ) ) )
23 19 22 anbi12d 
 |-  ( x = B -> ( ( <. B , C >. = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) <-> ( <. B , C >. = <. B , y >. /\ ( ( A .o B ) +o y ) = ( ( A .o B ) +o C ) ) ) )
24 opeq2 
 |-  ( y = C -> <. B , y >. = <. B , C >. )
25 24 eqeq2d 
 |-  ( y = C -> ( <. B , C >. = <. B , y >. <-> <. B , C >. = <. B , C >. ) )
26 oveq2 
 |-  ( y = C -> ( ( A .o B ) +o y ) = ( ( A .o B ) +o C ) )
27 26 eqeq1d 
 |-  ( y = C -> ( ( ( A .o B ) +o y ) = ( ( A .o B ) +o C ) <-> ( ( A .o B ) +o C ) = ( ( A .o B ) +o C ) ) )
28 25 27 anbi12d 
 |-  ( y = C -> ( ( <. B , C >. = <. B , y >. /\ ( ( A .o B ) +o y ) = ( ( A .o B ) +o C ) ) <-> ( <. B , C >. = <. B , C >. /\ ( ( A .o B ) +o C ) = ( ( A .o B ) +o C ) ) ) )
29 eqid 
 |-  <. B , C >. = <. B , C >.
30 eqid 
 |-  ( ( A .o B ) +o C ) = ( ( A .o B ) +o C )
31 29 30 pm3.2i 
 |-  ( <. B , C >. = <. B , C >. /\ ( ( A .o B ) +o C ) = ( ( A .o B ) +o C ) )
32 31 a1i 
 |-  ( ph -> ( <. B , C >. = <. B , C >. /\ ( ( A .o B ) +o C ) = ( ( A .o B ) +o C ) ) )
33 23 28 3 4 32 2rspcedvdw 
 |-  ( ph -> E. x e. On E. y e. A ( <. B , C >. = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) )
34 opeq1 
 |-  ( x = D -> <. x , y >. = <. D , y >. )
35 34 eqeq2d 
 |-  ( x = D -> ( <. D , E >. = <. x , y >. <-> <. D , E >. = <. D , y >. ) )
36 oveq2 
 |-  ( x = D -> ( A .o x ) = ( A .o D ) )
37 36 oveq1d 
 |-  ( x = D -> ( ( A .o x ) +o y ) = ( ( A .o D ) +o y ) )
38 37 eqeq1d 
 |-  ( x = D -> ( ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) <-> ( ( A .o D ) +o y ) = ( ( A .o B ) +o C ) ) )
39 35 38 anbi12d 
 |-  ( x = D -> ( ( <. D , E >. = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) <-> ( <. D , E >. = <. D , y >. /\ ( ( A .o D ) +o y ) = ( ( A .o B ) +o C ) ) ) )
40 opeq2 
 |-  ( y = E -> <. D , y >. = <. D , E >. )
41 40 eqeq2d 
 |-  ( y = E -> ( <. D , E >. = <. D , y >. <-> <. D , E >. = <. D , E >. ) )
42 oveq2 
 |-  ( y = E -> ( ( A .o D ) +o y ) = ( ( A .o D ) +o E ) )
43 42 eqeq1d 
 |-  ( y = E -> ( ( ( A .o D ) +o y ) = ( ( A .o B ) +o C ) <-> ( ( A .o D ) +o E ) = ( ( A .o B ) +o C ) ) )
44 41 43 anbi12d 
 |-  ( y = E -> ( ( <. D , E >. = <. D , y >. /\ ( ( A .o D ) +o y ) = ( ( A .o B ) +o C ) ) <-> ( <. D , E >. = <. D , E >. /\ ( ( A .o D ) +o E ) = ( ( A .o B ) +o C ) ) ) )
45 7 eqcomd 
 |-  ( ph -> ( ( A .o D ) +o E ) = ( ( A .o B ) +o C ) )
46 eqid 
 |-  <. D , E >. = <. D , E >.
47 45 46 jctil 
 |-  ( ph -> ( <. D , E >. = <. D , E >. /\ ( ( A .o D ) +o E ) = ( ( A .o B ) +o C ) ) )
48 39 44 5 6 47 2rspcedvdw 
 |-  ( ph -> E. x e. On E. y e. A ( <. D , E >. = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) )
49 opex 
 |-  <. B , C >. e. _V
50 opex 
 |-  <. D , E >. e. _V
51 49 50 pm3.2i 
 |-  ( <. B , C >. e. _V /\ <. D , E >. e. _V )
52 eqeq1 
 |-  ( z = <. B , C >. -> ( z = <. x , y >. <-> <. B , C >. = <. x , y >. ) )
53 52 anbi1d 
 |-  ( z = <. B , C >. -> ( ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) <-> ( <. B , C >. = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) ) )
54 53 2rexbidv 
 |-  ( z = <. B , C >. -> ( E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) <-> E. x e. On E. y e. A ( <. B , C >. = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) ) )
55 eqeq1 
 |-  ( z = <. D , E >. -> ( z = <. x , y >. <-> <. D , E >. = <. x , y >. ) )
56 55 anbi1d 
 |-  ( z = <. D , E >. -> ( ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) <-> ( <. D , E >. = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) ) )
57 56 2rexbidv 
 |-  ( z = <. D , E >. -> ( E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) <-> E. x e. On E. y e. A ( <. D , E >. = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) ) )
58 54 57 moi 
 |-  ( ( ( <. B , C >. e. _V /\ <. D , E >. e. _V ) /\ E* z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) /\ ( E. x e. On E. y e. A ( <. B , C >. = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) /\ E. x e. On E. y e. A ( <. D , E >. = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) ) ) -> <. B , C >. = <. D , E >. )
59 51 58 mp3an1 
 |-  ( ( E* z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) /\ ( E. x e. On E. y e. A ( <. B , C >. = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) /\ E. x e. On E. y e. A ( <. D , E >. = <. x , y >. /\ ( ( A .o x ) +o y ) = ( ( A .o B ) +o C ) ) ) ) -> <. B , C >. = <. D , E >. )
60 17 33 48 59 syl12anc 
 |-  ( ph -> <. B , C >. = <. D , E >. )
61 opthg 
 |-  ( ( B e. On /\ C e. A ) -> ( <. B , C >. = <. D , E >. <-> ( B = D /\ C = E ) ) )
62 3 4 61 syl2anc 
 |-  ( ph -> ( <. B , C >. = <. D , E >. <-> ( B = D /\ C = E ) ) )
63 60 62 mpbid 
 |-  ( ph -> ( B = D /\ C = E ) )