Theorem omltoe

Description: Exponentiation eventually dominates multiplication. (Contributed by RP, 3-Jan-2025)

	Ref	Expression
Assertion	omltoe	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐵 ·o 𝐴 ) ∈ ( 𝐵 ↑o 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐵 ∈ On )
2	1	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → 𝐵 ∈ On )
3		oe2	⊢ ( 𝐵 ∈ On → ( 𝐵 ·o 𝐵 ) = ( 𝐵 ↑o 2o ) )
4	2 3	syl	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → ( 𝐵 ·o 𝐵 ) = ( 𝐵 ↑o 2o ) )
5		2on	⊢ 2o ∈ On
6	5	a1i	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 2o ∈ On )
7		simpl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ∈ On )
8	6 7 1	3jca	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 2o ∈ On ∧ 𝐴 ∈ On ∧ 𝐵 ∈ On ) )
9	8	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → ( 2o ∈ On ∧ 𝐴 ∈ On ∧ 𝐵 ∈ On ) )
10		simpr	⊢ ( ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ 𝐵 )
11	10	adantl	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → 𝐴 ∈ 𝐵 )
12	11	ne0d	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → 𝐵 ≠ ∅ )
13		on0eln0	⊢ ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ 𝐵 ≠ ∅ ) )
14	2 13	syl	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → ( ∅ ∈ 𝐵 ↔ 𝐵 ≠ ∅ ) )
15	12 14	mpbird	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → ∅ ∈ 𝐵 )
16	9 15	jca	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → ( ( 2o ∈ On ∧ 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) )
17		df-2o	⊢ 2o = suc 1o
18	17	a1i	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → 2o = suc 1o )
19		simpl	⊢ ( ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) → 1o ∈ 𝐴 )
20	19	adantl	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → 1o ∈ 𝐴 )
21		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
22	21	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → Ord 𝐴 )
23	22	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → Ord 𝐴 )
24	20 23	jca	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → ( 1o ∈ 𝐴 ∧ Ord 𝐴 ) )
25		ordelsuc	⊢ ( ( 1o ∈ 𝐴 ∧ Ord 𝐴 ) → ( 1o ∈ 𝐴 ↔ suc 1o ⊆ 𝐴 ) )
26	25	biimpd	⊢ ( ( 1o ∈ 𝐴 ∧ Ord 𝐴 ) → ( 1o ∈ 𝐴 → suc 1o ⊆ 𝐴 ) )
27	24 20 26	sylc	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → suc 1o ⊆ 𝐴 )
28	18 27	eqsstrd	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → 2o ⊆ 𝐴 )
29		oewordi	⊢ ( ( ( 2o ∈ On ∧ 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → ( 2o ⊆ 𝐴 → ( 𝐵 ↑o 2o ) ⊆ ( 𝐵 ↑o 𝐴 ) ) )
30	16 28 29	sylc	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → ( 𝐵 ↑o 2o ) ⊆ ( 𝐵 ↑o 𝐴 ) )
31	4 30	eqsstrd	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → ( 𝐵 ·o 𝐵 ) ⊆ ( 𝐵 ↑o 𝐴 ) )
32	2 2 15	jca31	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → ( ( 𝐵 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) )
33		omordi	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → ( 𝐴 ∈ 𝐵 → ( 𝐵 ·o 𝐴 ) ∈ ( 𝐵 ·o 𝐵 ) ) )
34	32 11 33	sylc	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → ( 𝐵 ·o 𝐴 ) ∈ ( 𝐵 ·o 𝐵 ) )
35	31 34	sseldd	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) → ( 𝐵 ·o 𝐴 ) ∈ ( 𝐵 ↑o 𝐴 ) )
36	35	ex	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐵 ·o 𝐴 ) ∈ ( 𝐵 ↑o 𝐴 ) ) )