Metamath Proof Explorer

Theorem oenord1

Description: When two ordinals (both at least as large as two) are raised to the same power, ordering of the powers is not equivalent to the ordering of the bases. Remark 3.26 of Schloeder p. 11. (Contributed by RP, 4-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 oenord1ex 
 |-  -. ( 2o e. 3o <-> ( 2o ^o _om ) e. ( 3o ^o _om ) )
2 2on 
 |-  2o e. On
3 1oex 
 |-  1o e. _V
4 3 prid2 
 |-  1o e. { (/) , 1o }
5 df2o3 
 |-  2o = { (/) , 1o }
6 4 5 eleqtrri 
 |-  1o e. 2o
7 ondif2 
 |-  ( 2o e. ( On \ 2o ) <-> ( 2o e. On /\ 1o e. 2o ) )
8 2 6 7 mpbir2an 
 |-  2o e. ( On \ 2o )
9 3on 
 |-  3o e. On
10 3 tpid2 
 |-  1o e. { (/) , 1o , 2o }
11 df3o2 
 |-  3o = { (/) , 1o , 2o }
12 10 11 eleqtrri 
 |-  1o e. 3o
13 ondif2 
 |-  ( 3o e. ( On \ 2o ) <-> ( 3o e. On /\ 1o e. 3o ) )
14 9 12 13 mpbir2an 
 |-  3o e. ( On \ 2o )
15 omelon 
 |-  _om e. On
16 peano1 
 |-  (/) e. _om
17 ondif1 
 |-  ( _om e. ( On \ 1o ) <-> ( _om e. On /\ (/) e. _om ) )
18 15 16 17 mpbir2an 
 |-  _om e. ( On \ 1o )
19 oveq2 
 |-  ( c = _om -> ( 2o ^o c ) = ( 2o ^o _om ) )
20 oveq2 
 |-  ( c = _om -> ( 3o ^o c ) = ( 3o ^o _om ) )
21 19 20 eleq12d 
 |-  ( c = _om -> ( ( 2o ^o c ) e. ( 3o ^o c ) <-> ( 2o ^o _om ) e. ( 3o ^o _om ) ) )
22 21 bibi2d 
 |-  ( c = _om -> ( ( 2o e. 3o <-> ( 2o ^o c ) e. ( 3o ^o c ) ) <-> ( 2o e. 3o <-> ( 2o ^o _om ) e. ( 3o ^o _om ) ) ) )
23 22 notbid 
 |-  ( c = _om -> ( -. ( 2o e. 3o <-> ( 2o ^o c ) e. ( 3o ^o c ) ) <-> -. ( 2o e. 3o <-> ( 2o ^o _om ) e. ( 3o ^o _om ) ) ) )
24 23 rspcev 
 |-  ( ( _om e. ( On \ 1o ) /\ -. ( 2o e. 3o <-> ( 2o ^o _om ) e. ( 3o ^o _om ) ) ) -> E. c e. ( On \ 1o ) -. ( 2o e. 3o <-> ( 2o ^o c ) e. ( 3o ^o c ) ) )
25 18 24 mpan 
 |-  ( -. ( 2o e. 3o <-> ( 2o ^o _om ) e. ( 3o ^o _om ) ) -> E. c e. ( On \ 1o ) -. ( 2o e. 3o <-> ( 2o ^o c ) e. ( 3o ^o c ) ) )
26 eleq2 
 |-  ( b = 3o -> ( 2o e. b <-> 2o e. 3o ) )
27 oveq1 
 |-  ( b = 3o -> ( b ^o c ) = ( 3o ^o c ) )
28 27 eleq2d 
 |-  ( b = 3o -> ( ( 2o ^o c ) e. ( b ^o c ) <-> ( 2o ^o c ) e. ( 3o ^o c ) ) )
29 26 28 bibi12d 
 |-  ( b = 3o -> ( ( 2o e. b <-> ( 2o ^o c ) e. ( b ^o c ) ) <-> ( 2o e. 3o <-> ( 2o ^o c ) e. ( 3o ^o c ) ) ) )
30 29 notbid 
 |-  ( b = 3o -> ( -. ( 2o e. b <-> ( 2o ^o c ) e. ( b ^o c ) ) <-> -. ( 2o e. 3o <-> ( 2o ^o c ) e. ( 3o ^o c ) ) ) )
31 30 rexbidv 
 |-  ( b = 3o -> ( E. c e. ( On \ 1o ) -. ( 2o e. b <-> ( 2o ^o c ) e. ( b ^o c ) ) <-> E. c e. ( On \ 1o ) -. ( 2o e. 3o <-> ( 2o ^o c ) e. ( 3o ^o c ) ) ) )
32 31 rspcev 
 |-  ( ( 3o e. ( On \ 2o ) /\ E. c e. ( On \ 1o ) -. ( 2o e. 3o <-> ( 2o ^o c ) e. ( 3o ^o c ) ) ) -> E. b e. ( On \ 2o ) E. c e. ( On \ 1o ) -. ( 2o e. b <-> ( 2o ^o c ) e. ( b ^o c ) ) )
33 14 25 32 sylancr 
 |-  ( -. ( 2o e. 3o <-> ( 2o ^o _om ) e. ( 3o ^o _om ) ) -> E. b e. ( On \ 2o ) E. c e. ( On \ 1o ) -. ( 2o e. b <-> ( 2o ^o c ) e. ( b ^o c ) ) )
34 eleq1 
 |-  ( a = 2o -> ( a e. b <-> 2o e. b ) )
35 oveq1 
 |-  ( a = 2o -> ( a ^o c ) = ( 2o ^o c ) )
36 35 eleq1d 
 |-  ( a = 2o -> ( ( a ^o c ) e. ( b ^o c ) <-> ( 2o ^o c ) e. ( b ^o c ) ) )
37 34 36 bibi12d 
 |-  ( a = 2o -> ( ( a e. b <-> ( a ^o c ) e. ( b ^o c ) ) <-> ( 2o e. b <-> ( 2o ^o c ) e. ( b ^o c ) ) ) )
38 37 notbid 
 |-  ( a = 2o -> ( -. ( a e. b <-> ( a ^o c ) e. ( b ^o c ) ) <-> -. ( 2o e. b <-> ( 2o ^o c ) e. ( b ^o c ) ) ) )
39 38 2rexbidv 
 |-  ( a = 2o -> ( E. b e. ( On \ 2o ) E. c e. ( On \ 1o ) -. ( a e. b <-> ( a ^o c ) e. ( b ^o c ) ) <-> E. b e. ( On \ 2o ) E. c e. ( On \ 1o ) -. ( 2o e. b <-> ( 2o ^o c ) e. ( b ^o c ) ) ) )
40 39 rspcev 
 |-  ( ( 2o e. ( On \ 2o ) /\ E. b e. ( On \ 2o ) E. c e. ( On \ 1o ) -. ( 2o e. b <-> ( 2o ^o c ) e. ( b ^o c ) ) ) -> E. a e. ( On \ 2o ) E. b e. ( On \ 2o ) E. c e. ( On \ 1o ) -. ( a e. b <-> ( a ^o c ) e. ( b ^o c ) ) )
41 8 33 40 sylancr 
 |-  ( -. ( 2o e. 3o <-> ( 2o ^o _om ) e. ( 3o ^o _om ) ) -> E. a e. ( On \ 2o ) E. b e. ( On \ 2o ) E. c e. ( On \ 1o ) -. ( a e. b <-> ( a ^o c ) e. ( b ^o c ) ) )
42 1 41 ax-mp 
 |-  E. a e. ( On \ 2o ) E. b e. ( On \ 2o ) E. c e. ( On \ 1o ) -. ( a e. b <-> ( a ^o c ) e. ( b ^o c ) )