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 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ ω ∖ 1 𝑜 ∧ D ∈ ω ∖ 1 𝑜 → A ∈ B → ω ↑ 𝑜 A ⋅ 𝑜 C ∈ ω ↑ 𝑜 B ⋅ 𝑜 D

Proof

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