Metamath Proof Explorer

Theorem omnord1

Description: When the same non-zero ordinal is multiplied on the right, ordering of the products is not equivalent to the ordering of the ordinals on the left. Remark 3.18 of Schloeder p. 10. (Contributed by RP, 4-Feb-2025)

Ref Expression
Assertion omnord1 
|- E. a e. On E. b e. On E. c e. ( On \ 1o ) -. ( a e. b <-> ( a .o c ) e. ( b .o c ) )

Proof

Step Hyp Ref Expression
1 omnord1ex 
 |-  -. ( 1o e. 2o <-> ( 1o .o _om ) e. ( 2o .o _om ) )
2 1on 
 |-  1o e. On
3 2on 
 |-  2o e. On
4 omelon 
 |-  _om e. On
5 peano1 
 |-  (/) e. _om
6 ondif1 
 |-  ( _om e. ( On \ 1o ) <-> ( _om e. On /\ (/) e. _om ) )
7 4 5 6 mpbir2an 
 |-  _om e. ( On \ 1o )
8 oveq2 
 |-  ( c = _om -> ( 1o .o c ) = ( 1o .o _om ) )
9 oveq2 
 |-  ( c = _om -> ( 2o .o c ) = ( 2o .o _om ) )
10 8 9 eleq12d 
 |-  ( c = _om -> ( ( 1o .o c ) e. ( 2o .o c ) <-> ( 1o .o _om ) e. ( 2o .o _om ) ) )
11 10 bibi2d 
 |-  ( c = _om -> ( ( 1o e. 2o <-> ( 1o .o c ) e. ( 2o .o c ) ) <-> ( 1o e. 2o <-> ( 1o .o _om ) e. ( 2o .o _om ) ) ) )
12 11 notbid 
 |-  ( c = _om -> ( -. ( 1o e. 2o <-> ( 1o .o c ) e. ( 2o .o c ) ) <-> -. ( 1o e. 2o <-> ( 1o .o _om ) e. ( 2o .o _om ) ) ) )
13 12 rspcev 
 |-  ( ( _om e. ( On \ 1o ) /\ -. ( 1o e. 2o <-> ( 1o .o _om ) e. ( 2o .o _om ) ) ) -> E. c e. ( On \ 1o ) -. ( 1o e. 2o <-> ( 1o .o c ) e. ( 2o .o c ) ) )
14 7 13 mpan 
 |-  ( -. ( 1o e. 2o <-> ( 1o .o _om ) e. ( 2o .o _om ) ) -> E. c e. ( On \ 1o ) -. ( 1o e. 2o <-> ( 1o .o c ) e. ( 2o .o c ) ) )
15 eleq2 
 |-  ( b = 2o -> ( 1o e. b <-> 1o e. 2o ) )
16 oveq1 
 |-  ( b = 2o -> ( b .o c ) = ( 2o .o c ) )
17 16 eleq2d 
 |-  ( b = 2o -> ( ( 1o .o c ) e. ( b .o c ) <-> ( 1o .o c ) e. ( 2o .o c ) ) )
18 15 17 bibi12d 
 |-  ( b = 2o -> ( ( 1o e. b <-> ( 1o .o c ) e. ( b .o c ) ) <-> ( 1o e. 2o <-> ( 1o .o c ) e. ( 2o .o c ) ) ) )
19 18 notbid 
 |-  ( b = 2o -> ( -. ( 1o e. b <-> ( 1o .o c ) e. ( b .o c ) ) <-> -. ( 1o e. 2o <-> ( 1o .o c ) e. ( 2o .o c ) ) ) )
20 19 rexbidv 
 |-  ( b = 2o -> ( E. c e. ( On \ 1o ) -. ( 1o e. b <-> ( 1o .o c ) e. ( b .o c ) ) <-> E. c e. ( On \ 1o ) -. ( 1o e. 2o <-> ( 1o .o c ) e. ( 2o .o c ) ) ) )
21 20 rspcev 
 |-  ( ( 2o e. On /\ E. c e. ( On \ 1o ) -. ( 1o e. 2o <-> ( 1o .o c ) e. ( 2o .o c ) ) ) -> E. b e. On E. c e. ( On \ 1o ) -. ( 1o e. b <-> ( 1o .o c ) e. ( b .o c ) ) )
22 3 14 21 sylancr 
 |-  ( -. ( 1o e. 2o <-> ( 1o .o _om ) e. ( 2o .o _om ) ) -> E. b e. On E. c e. ( On \ 1o ) -. ( 1o e. b <-> ( 1o .o c ) e. ( b .o c ) ) )
23 eleq1 
 |-  ( a = 1o -> ( a e. b <-> 1o e. b ) )
24 oveq1 
 |-  ( a = 1o -> ( a .o c ) = ( 1o .o c ) )
25 24 eleq1d 
 |-  ( a = 1o -> ( ( a .o c ) e. ( b .o c ) <-> ( 1o .o c ) e. ( b .o c ) ) )
26 23 25 bibi12d 
 |-  ( a = 1o -> ( ( a e. b <-> ( a .o c ) e. ( b .o c ) ) <-> ( 1o e. b <-> ( 1o .o c ) e. ( b .o c ) ) ) )
27 26 notbid 
 |-  ( a = 1o -> ( -. ( a e. b <-> ( a .o c ) e. ( b .o c ) ) <-> -. ( 1o e. b <-> ( 1o .o c ) e. ( b .o c ) ) ) )
28 27 rexbidv 
 |-  ( a = 1o -> ( E. c e. ( On \ 1o ) -. ( a e. b <-> ( a .o c ) e. ( b .o c ) ) <-> E. c e. ( On \ 1o ) -. ( 1o e. b <-> ( 1o .o c ) e. ( b .o c ) ) ) )
29 28 rexbidv 
 |-  ( a = 1o -> ( E. b e. On E. c e. ( On \ 1o ) -. ( a e. b <-> ( a .o c ) e. ( b .o c ) ) <-> E. b e. On E. c e. ( On \ 1o ) -. ( 1o e. b <-> ( 1o .o c ) e. ( b .o c ) ) ) )
30 29 rspcev 
 |-  ( ( 1o e. On /\ E. b e. On E. c e. ( On \ 1o ) -. ( 1o e. b <-> ( 1o .o c ) e. ( b .o c ) ) ) -> E. a e. On E. b e. On E. c e. ( On \ 1o ) -. ( a e. b <-> ( a .o c ) e. ( b .o c ) ) )
31 2 22 30 sylancr 
 |-  ( -. ( 1o e. 2o <-> ( 1o .o _om ) e. ( 2o .o _om ) ) -> E. a e. On E. b e. On E. c e. ( On \ 1o ) -. ( a e. b <-> ( a .o c ) e. ( b .o c ) ) )
32 1 31 ax-mp 
 |-  E. a e. On E. b e. On E. c e. ( On \ 1o ) -. ( a e. b <-> ( a .o c ) e. ( b .o c ) )