Metamath Proof Explorer

Theorem oaltom

Description: Multiplication eventually dominates addition. (Contributed by RP, 3-Jan-2025)

Ref Expression
Assertion oaltom ⊢ A ∈ On ∧ B ∈ On → 1 𝑜 ∈ A ∧ A ∈ B → B + 𝑜 A ∈ B ⋅ 𝑜 A

Proof

Step Hyp Ref Expression
1 om2 ⊢ B ∈ On → B + 𝑜 B = B ⋅ 𝑜 2 𝑜
2 1 ad2antlr ⊢ A ∈ On ∧ B ∈ On ∧ 1 𝑜 ∈ A ∧ A ∈ B → B + 𝑜 B = B ⋅ 𝑜 2 𝑜
3 2on ⊢ 2 𝑜 ∈ On
4 3 a1i ⊢ A ∈ On ∧ B ∈ On → 2 𝑜 ∈ On
5 simpl ⊢ A ∈ On ∧ B ∈ On → A ∈ On
6 simpr ⊢ A ∈ On ∧ B ∈ On → B ∈ On
7 4 5 6 3jca ⊢ A ∈ On ∧ B ∈ On → 2 𝑜 ∈ On ∧ A ∈ On ∧ B ∈ On
8 7 adantr ⊢ A ∈ On ∧ B ∈ On ∧ 1 𝑜 ∈ A ∧ A ∈ B → 2 𝑜 ∈ On ∧ A ∈ On ∧ B ∈ On
9 df-2o ⊢ 2 𝑜 = suc ⁡ 1 𝑜
10 9 a1i ⊢ A ∈ On ∧ B ∈ On ∧ 1 𝑜 ∈ A ∧ A ∈ B → 2 𝑜 = suc ⁡ 1 𝑜
11 simprl ⊢ A ∈ On ∧ B ∈ On ∧ 1 𝑜 ∈ A ∧ A ∈ B → 1 𝑜 ∈ A
12 eloni ⊢ A ∈ On → Ord ⁡ A
13 12 adantr ⊢ A ∈ On ∧ B ∈ On → Ord ⁡ A
14 13 adantr ⊢ A ∈ On ∧ B ∈ On ∧ 1 𝑜 ∈ A ∧ A ∈ B → Ord ⁡ A
15 11 14 jca ⊢ A ∈ On ∧ B ∈ On ∧ 1 𝑜 ∈ A ∧ A ∈ B → 1 𝑜 ∈ A ∧ Ord ⁡ A
16 ordelsuc ⊢ 1 𝑜 ∈ A ∧ Ord ⁡ A → 1 𝑜 ∈ A ↔ suc ⁡ 1 𝑜 ⊆ A
17 16 biimpd ⊢ 1 𝑜 ∈ A ∧ Ord ⁡ A → 1 𝑜 ∈ A → suc ⁡ 1 𝑜 ⊆ A
18 15 11 17 sylc ⊢ A ∈ On ∧ B ∈ On ∧ 1 𝑜 ∈ A ∧ A ∈ B → suc ⁡ 1 𝑜 ⊆ A
19 10 18 eqsstrd ⊢ A ∈ On ∧ B ∈ On ∧ 1 𝑜 ∈ A ∧ A ∈ B → 2 𝑜 ⊆ A
20 omwordi ⊢ 2 𝑜 ∈ On ∧ A ∈ On ∧ B ∈ On → 2 𝑜 ⊆ A → B ⋅ 𝑜 2 𝑜 ⊆ B ⋅ 𝑜 A
21 8 19 20 sylc ⊢ A ∈ On ∧ B ∈ On ∧ 1 𝑜 ∈ A ∧ A ∈ B → B ⋅ 𝑜 2 𝑜 ⊆ B ⋅ 𝑜 A
22 2 21 eqsstrd ⊢ A ∈ On ∧ B ∈ On ∧ 1 𝑜 ∈ A ∧ A ∈ B → B + 𝑜 B ⊆ B ⋅ 𝑜 A
23 6 6 jca ⊢ A ∈ On ∧ B ∈ On → B ∈ On ∧ B ∈ On
24 simpr ⊢ 1 𝑜 ∈ A ∧ A ∈ B → A ∈ B
25 oaordi ⊢ B ∈ On ∧ B ∈ On → A ∈ B → B + 𝑜 A ∈ B + 𝑜 B
26 25 imp ⊢ B ∈ On ∧ B ∈ On ∧ A ∈ B → B + 𝑜 A ∈ B + 𝑜 B
27 23 24 26 syl2an ⊢ A ∈ On ∧ B ∈ On ∧ 1 𝑜 ∈ A ∧ A ∈ B → B + 𝑜 A ∈ B + 𝑜 B
28 22 27 sseldd ⊢ A ∈ On ∧ B ∈ On ∧ 1 𝑜 ∈ A ∧ A ∈ B → B + 𝑜 A ∈ B ⋅ 𝑜 A
29 28 ex ⊢ A ∈ On ∧ B ∈ On → 1 𝑜 ∈ A ∧ A ∈ B → B + 𝑜 A ∈ B ⋅ 𝑜 A