Metamath Proof Explorer

Theorem cantnftermord

Description: For terms of the form of a power of omega times a non-zero natural number, ordering of the exponents implies ordering of the terms. Lemma 5.1 of Schloeder p. 15. (Contributed by RP, 30-Jan-2025)

Ref Expression
Assertion cantnftermord 
|- ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) -> ( A e. B -> ( ( _om ^o A ) .o C ) e. ( ( _om ^o B ) .o D ) ) )

Proof

Step Hyp Ref Expression
1 simplll 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> A e. On )
2 onsuc 
 |-  ( A e. On -> suc A e. On )
3 1 2 syl 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> suc A e. On )
4 simpllr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> B e. On )
5 omelon 
 |-  _om e. On
6 1onn 
 |-  1o e. _om
7 ondif2 
 |-  ( _om e. ( On \ 2o ) <-> ( _om e. On /\ 1o e. _om ) )
8 5 6 7 mpbir2an 
 |-  _om e. ( On \ 2o )
9 8 a1i 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> _om e. ( On \ 2o ) )
10 onsucss 
 |-  ( B e. On -> ( A e. B -> suc A C_ B ) )
11 10 ad2antlr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) -> ( A e. B -> suc A C_ B ) )
12 11 imp 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> suc A C_ B )
13 oeword 
 |-  ( ( suc A e. On /\ B e. On /\ _om e. ( On \ 2o ) ) -> ( suc A C_ B <-> ( _om ^o suc A ) C_ ( _om ^o B ) ) )
14 13 biimpa 
 |-  ( ( ( suc A e. On /\ B e. On /\ _om e. ( On \ 2o ) ) /\ suc A C_ B ) -> ( _om ^o suc A ) C_ ( _om ^o B ) )
15 3 4 9 12 14 syl31anc 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> ( _om ^o suc A ) C_ ( _om ^o B ) )
16 5 a1i 
 |-  ( ( A e. On /\ B e. On ) -> _om e. On )
17 oecl 
 |-  ( ( _om e. On /\ B e. On ) -> ( _om ^o B ) e. On )
18 16 17 sylancom 
 |-  ( ( A e. On /\ B e. On ) -> ( _om ^o B ) e. On )
19 omsson 
 |-  _om C_ On
20 ssdif 
 |-  ( _om C_ On -> ( _om \ 1o ) C_ ( On \ 1o ) )
21 19 20 ax-mp 
 |-  ( _om \ 1o ) C_ ( On \ 1o )
22 21 sseli 
 |-  ( D e. ( _om \ 1o ) -> D e. ( On \ 1o ) )
23 ondif1 
 |-  ( D e. ( On \ 1o ) <-> ( D e. On /\ (/) e. D ) )
24 22 23 sylib 
 |-  ( D e. ( _om \ 1o ) -> ( D e. On /\ (/) e. D ) )
25 24 adantl 
 |-  ( ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) -> ( D e. On /\ (/) e. D ) )
26 18 25 anim12i 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) -> ( ( _om ^o B ) e. On /\ ( D e. On /\ (/) e. D ) ) )
27 26 adantr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> ( ( _om ^o B ) e. On /\ ( D e. On /\ (/) e. D ) ) )
28 anass 
 |-  ( ( ( ( _om ^o B ) e. On /\ D e. On ) /\ (/) e. D ) <-> ( ( _om ^o B ) e. On /\ ( D e. On /\ (/) e. D ) ) )
29 27 28 sylibr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> ( ( ( _om ^o B ) e. On /\ D e. On ) /\ (/) e. D ) )
30 omword1 
 |-  ( ( ( ( _om ^o B ) e. On /\ D e. On ) /\ (/) e. D ) -> ( _om ^o B ) C_ ( ( _om ^o B ) .o D ) )
31 29 30 syl 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> ( _om ^o B ) C_ ( ( _om ^o B ) .o D ) )
32 15 31 sstrd 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> ( _om ^o suc A ) C_ ( ( _om ^o B ) .o D ) )
33 5 a1i 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> _om e. On )
34 1 5 jctil 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> ( _om e. On /\ A e. On ) )
35 oecl 
 |-  ( ( _om e. On /\ A e. On ) -> ( _om ^o A ) e. On )
36 34 35 syl 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> ( _om ^o A ) e. On )
37 peano1 
 |-  (/) e. _om
38 oen0 
 |-  ( ( ( _om e. On /\ A e. On ) /\ (/) e. _om ) -> (/) e. ( _om ^o A ) )
39 34 37 38 sylancl 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> (/) e. ( _om ^o A ) )
40 simplrl 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> C e. ( _om \ 1o ) )
41 40 eldifad 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> C e. _om )
42 omordi 
 |-  ( ( ( _om e. On /\ ( _om ^o A ) e. On ) /\ (/) e. ( _om ^o A ) ) -> ( C e. _om -> ( ( _om ^o A ) .o C ) e. ( ( _om ^o A ) .o _om ) ) )
43 42 imp 
 |-  ( ( ( ( _om e. On /\ ( _om ^o A ) e. On ) /\ (/) e. ( _om ^o A ) ) /\ C e. _om ) -> ( ( _om ^o A ) .o C ) e. ( ( _om ^o A ) .o _om ) )
44 33 36 39 41 43 syl1111anc 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> ( ( _om ^o A ) .o C ) e. ( ( _om ^o A ) .o _om ) )
45 oesuc 
 |-  ( ( _om e. On /\ A e. On ) -> ( _om ^o suc A ) = ( ( _om ^o A ) .o _om ) )
46 34 45 syl 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> ( _om ^o suc A ) = ( ( _om ^o A ) .o _om ) )
47 44 46 eleqtrrd 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> ( ( _om ^o A ) .o C ) e. ( _om ^o suc A ) )
48 32 47 sseldd 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) /\ A e. B ) -> ( ( _om ^o A ) .o C ) e. ( ( _om ^o B ) .o D ) )
49 48 ex 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. ( _om \ 1o ) /\ D e. ( _om \ 1o ) ) ) -> ( A e. B -> ( ( _om ^o A ) .o C ) e. ( ( _om ^o B ) .o D ) ) )