Metamath Proof Explorer

Theorem cantnftermord

Description: For terms of the form of a power of omega times a nonzero 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 ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) → ( 𝐴 ∈ 𝐵 → ( ( ω ↑o 𝐴 ) ·o 𝐶 ) ∈ ( ( ω ↑o 𝐵 ) ·o 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 simplll ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ On )
2 onsuc ⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ On )
3 1 2 syl ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → suc 𝐴 ∈ On )
4 simpllr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → 𝐵 ∈ On )
5 omelon ⊢ ω ∈ On
6 1onn ⊢ 1o ∈ ω
7 ondif2 ⊢ ( ω ∈ ( On ∖ 2o ) ↔ ( ω ∈ On ∧ 1o ∈ ω ) )
8 5 6 7 mpbir2an ⊢ ω ∈ ( On ∖ 2o )
9 8 a1i ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → ω ∈ ( On ∖ 2o ) )
10 onsucss ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) )
11 10 ad2antlr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) )
12 11 imp ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → suc 𝐴 ⊆ 𝐵 )
13 oeword ⊢ ( ( suc 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ ω ∈ ( On ∖ 2o ) ) → ( suc 𝐴 ⊆ 𝐵 ↔ ( ω ↑o suc 𝐴 ) ⊆ ( ω ↑o 𝐵 ) ) )
14 13 biimpa ⊢ ( ( ( suc 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ ω ∈ ( On ∖ 2o ) ) ∧ suc 𝐴 ⊆ 𝐵 ) → ( ω ↑o suc 𝐴 ) ⊆ ( ω ↑o 𝐵 ) )
15 3 4 9 12 14 syl31anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ω ↑o suc 𝐴 ) ⊆ ( ω ↑o 𝐵 ) )
16 5 a1i ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ω ∈ On )
17 oecl ⊢ ( ( ω ∈ On ∧ 𝐵 ∈ On ) → ( ω ↑o 𝐵 ) ∈ On )
18 16 17 sylancom ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ω ↑o 𝐵 ) ∈ On )
19 omsson ⊢ ω ⊆ On
20 ssdif ⊢ ( ω ⊆ On → ( ω ∖ 1o ) ⊆ ( On ∖ 1o ) )
21 19 20 ax-mp ⊢ ( ω ∖ 1o ) ⊆ ( On ∖ 1o )
22 21 sseli ⊢ ( 𝐷 ∈ ( ω ∖ 1o ) → 𝐷 ∈ ( On ∖ 1o ) )
23 ondif1 ⊢ ( 𝐷 ∈ ( On ∖ 1o ) ↔ ( 𝐷 ∈ On ∧ ∅ ∈ 𝐷 ) )
24 22 23 sylib ⊢ ( 𝐷 ∈ ( ω ∖ 1o ) → ( 𝐷 ∈ On ∧ ∅ ∈ 𝐷 ) )
25 24 adantl ⊢ ( ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) → ( 𝐷 ∈ On ∧ ∅ ∈ 𝐷 ) )
26 18 25 anim12i ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) → ( ( ω ↑o 𝐵 ) ∈ On ∧ ( 𝐷 ∈ On ∧ ∅ ∈ 𝐷 ) ) )
27 26 adantr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ( ω ↑o 𝐵 ) ∈ On ∧ ( 𝐷 ∈ On ∧ ∅ ∈ 𝐷 ) ) )
28 anass ⊢ ( ( ( ( ω ↑o 𝐵 ) ∈ On ∧ 𝐷 ∈ On ) ∧ ∅ ∈ 𝐷 ) ↔ ( ( ω ↑o 𝐵 ) ∈ On ∧ ( 𝐷 ∈ On ∧ ∅ ∈ 𝐷 ) ) )
29 27 28 sylibr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ( ( ω ↑o 𝐵 ) ∈ On ∧ 𝐷 ∈ On ) ∧ ∅ ∈ 𝐷 ) )
30 omword1 ⊢ ( ( ( ( ω ↑o 𝐵 ) ∈ On ∧ 𝐷 ∈ On ) ∧ ∅ ∈ 𝐷 ) → ( ω ↑o 𝐵 ) ⊆ ( ( ω ↑o 𝐵 ) ·o 𝐷 ) )
31 29 30 syl ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ω ↑o 𝐵 ) ⊆ ( ( ω ↑o 𝐵 ) ·o 𝐷 ) )
32 15 31 sstrd ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ω ↑o suc 𝐴 ) ⊆ ( ( ω ↑o 𝐵 ) ·o 𝐷 ) )
33 5 a1i ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → ω ∈ On )
34 1 5 jctil ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ω ∈ On ∧ 𝐴 ∈ On ) )
35 oecl ⊢ ( ( ω ∈ On ∧ 𝐴 ∈ On ) → ( ω ↑o 𝐴 ) ∈ On )
36 34 35 syl ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ω ↑o 𝐴 ) ∈ On )
37 peano1 ⊢ ∅ ∈ ω
38 oen0 ⊢ ( ( ( ω ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ ω ) → ∅ ∈ ( ω ↑o 𝐴 ) )
39 34 37 38 sylancl ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → ∅ ∈ ( ω ↑o 𝐴 ) )
40 simplrl ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → 𝐶 ∈ ( ω ∖ 1o ) )
41 40 eldifad ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → 𝐶 ∈ ω )
42 omordi ⊢ ( ( ( ω ∈ On ∧ ( ω ↑o 𝐴 ) ∈ On ) ∧ ∅ ∈ ( ω ↑o 𝐴 ) ) → ( 𝐶 ∈ ω → ( ( ω ↑o 𝐴 ) ·o 𝐶 ) ∈ ( ( ω ↑o 𝐴 ) ·o ω ) ) )
43 42 imp ⊢ ( ( ( ( ω ∈ On ∧ ( ω ↑o 𝐴 ) ∈ On ) ∧ ∅ ∈ ( ω ↑o 𝐴 ) ) ∧ 𝐶 ∈ ω ) → ( ( ω ↑o 𝐴 ) ·o 𝐶 ) ∈ ( ( ω ↑o 𝐴 ) ·o ω ) )
44 33 36 39 41 43 syl1111anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ( ω ↑o 𝐴 ) ·o 𝐶 ) ∈ ( ( ω ↑o 𝐴 ) ·o ω ) )
45 oesuc ⊢ ( ( ω ∈ On ∧ 𝐴 ∈ On ) → ( ω ↑o suc 𝐴 ) = ( ( ω ↑o 𝐴 ) ·o ω ) )
46 34 45 syl ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ω ↑o suc 𝐴 ) = ( ( ω ↑o 𝐴 ) ·o ω ) )
47 44 46 eleqtrrd ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ( ω ↑o 𝐴 ) ·o 𝐶 ) ∈ ( ω ↑o suc 𝐴 ) )
48 32 47 sseldd ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ( ω ↑o 𝐴 ) ·o 𝐶 ) ∈ ( ( ω ↑o 𝐵 ) ·o 𝐷 ) )
49 48 ex ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ ( ω ∖ 1o ) ∧ 𝐷 ∈ ( ω ∖ 1o ) ) ) → ( 𝐴 ∈ 𝐵 → ( ( ω ↑o 𝐴 ) ·o 𝐶 ) ∈ ( ( ω ↑o 𝐵 ) ·o 𝐷 ) ) )