Metamath Proof Explorer

Theorem oaordnr

Description: When the same ordinal is added on the right, ordering of the sums is not equivalent to the ordering of the ordinals on the left. Remark 3.9 of Schloeder p. 8. (Contributed by RP, 29-Jan-2025)

Ref Expression
Assertion oaordnr 
|- E. a e. On E. b e. On E. c e. On -. ( a e. b <-> ( a +o c ) e. ( b +o c ) )

Proof

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