omltoe

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

		Ref	Expression
	Assertion	omltoe	$⊢ (A \in On \land B \in On) \to ((1_{𝑜} \in A \land A \in B) \to B \cdot_{𝑜} A \in (B ↑_{𝑜} A))$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (A \in On \land B \in On) \to B \in On$
2	1	adantr	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to B \in On$
3		oe2	$⊢ B \in On \to B \cdot_{𝑜} B = B ↑_{𝑜} 2_{𝑜}$
4	2 3	syl	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to B \cdot_{𝑜} B = B ↑_{𝑜} 2_{𝑜}$
5		2on	$⊢ 2_{𝑜} \in On$
6	5	a1i	$⊢ (A \in On \land B \in On) \to 2_{𝑜} \in On$
7		simpl	$⊢ (A \in On \land B \in On) \to A \in On$
8	6 7 1	3jca	$⊢ (A \in On \land B \in On) \to (2_{𝑜} \in On \land A \in On \land B \in On)$
9	8	adantr	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to (2_{𝑜} \in On \land A \in On \land B \in On)$
10		simpr	$⊢ (1_{𝑜} \in A \land A \in B) \to A \in B$
11	10	adantl	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to A \in B$
12	11	ne0d	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to B \neq \emptyset$
13		on0eln0	$⊢ B \in On \to (\emptyset \in B \leftrightarrow B \neq \emptyset)$
14	2 13	syl	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to (\emptyset \in B \leftrightarrow B \neq \emptyset)$
15	12 14	mpbird	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to \emptyset \in B$
16	9 15	jca	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to ((2_{𝑜} \in On \land A \in On \land B \in On) \land \emptyset \in B)$
17		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
18	17	a1i	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to 2_{𝑜} = suc 1_{𝑜}$
19		simpl	$⊢ (1_{𝑜} \in A \land A \in B) \to 1_{𝑜} \in A$
20	19	adantl	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to 1_{𝑜} \in A$
21		eloni	$⊢ A \in On \to Ord A$
22	21	adantr	$⊢ (A \in On \land B \in On) \to Ord A$
23	22	adantr	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to Ord A$
24	20 23	jca	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to (1_{𝑜} \in A \land Ord A)$
25		ordelsuc	$⊢ (1_{𝑜} \in A \land Ord A) \to (1_{𝑜} \in A \leftrightarrow suc 1_{𝑜} \subseteq A)$
26	25	biimpd	$⊢ (1_{𝑜} \in A \land Ord A) \to (1_{𝑜} \in A \to suc 1_{𝑜} \subseteq A)$
27	24 20 26	sylc	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to suc 1_{𝑜} \subseteq A$
28	18 27	eqsstrd	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to 2_{𝑜} \subseteq A$
29		oewordi	$⊢ ((2_{𝑜} \in On \land A \in On \land B \in On) \land \emptyset \in B) \to (2_{𝑜} \subseteq A \to B ↑_{𝑜} 2_{𝑜} \subseteq B ↑_{𝑜} A)$
30	16 28 29	sylc	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to B ↑_{𝑜} 2_{𝑜} \subseteq B ↑_{𝑜} A$
31	4 30	eqsstrd	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to B \cdot_{𝑜} B \subseteq B ↑_{𝑜} A$
32	2 2 15	jca31	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to ((B \in On \land B \in On) \land \emptyset \in B)$
33		omordi	$⊢ ((B \in On \land B \in On) \land \emptyset \in B) \to (A \in B \to B \cdot_{𝑜} A \in (B \cdot_{𝑜} B))$
34	32 11 33	sylc	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to B \cdot_{𝑜} A \in (B \cdot_{𝑜} B)$
35	31 34	sseldd	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to B \cdot_{𝑜} A \in (B ↑_{𝑜} A)$
36	35	ex	$⊢ (A \in On \land B \in On) \to ((1_{𝑜} \in A \land A \in B) \to B \cdot_{𝑜} A \in (B ↑_{𝑜} A))$

Metamath Proof Explorer

Theorem omltoe

Proof