Theorem oaltom

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

	Ref	Expression
Assertion	oaltom	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐵 +o 𝐴 ) ∈ ( 𝐵 ·o 𝐴 ) ) )

Proof

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