oege2

Description: Any power of an ordinal at least as large as two is greater-than-or-equal to the term on the right. Lemma 3.20 of Schloeder p. 10. See oeworde . (Contributed by RP, 29-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		2on	$⊢ 2_{𝑜} \in On$
2		1oex	$⊢ 1_{𝑜} \in V$
3	2	prid2	$⊢ 1_{𝑜} \in \{\emptyset, 1_{𝑜}\}$
4		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
5	3 4	eleqtrri	$⊢ 1_{𝑜} \in 2_{𝑜}$
6		ondif2	$⊢ 2_{𝑜} \in (On ∖ 2_{𝑜}) \leftrightarrow (2_{𝑜} \in On \land 1_{𝑜} \in 2_{𝑜})$
7	1 5 6	mpbir2an	$⊢ 2_{𝑜} \in (On ∖ 2_{𝑜})$
8		oeworde	$⊢ (2_{𝑜} \in (On ∖ 2_{𝑜}) \land B \in On) \to B \subseteq 2_{𝑜} ↑_{𝑜} B$
9	7 8	mpan	$⊢ B \in On \to B \subseteq 2_{𝑜} ↑_{𝑜} B$
10	9	adantl	$⊢ ((A \in On \land 1_{𝑜} \in A) \land B \in On) \to B \subseteq 2_{𝑜} ↑_{𝑜} B$
11		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
12		onsucss	$⊢ A \in On \to (1_{𝑜} \in A \to suc 1_{𝑜} \subseteq A)$
13	12	imp	$⊢ (A \in On \land 1_{𝑜} \in A) \to suc 1_{𝑜} \subseteq A$
14	13	adantr	$⊢ ((A \in On \land 1_{𝑜} \in A) \land B \in On) \to suc 1_{𝑜} \subseteq A$
15	11 14	eqsstrid	$⊢ ((A \in On \land 1_{𝑜} \in A) \land B \in On) \to 2_{𝑜} \subseteq A$
16		simpll	$⊢ ((A \in On \land 1_{𝑜} \in A) \land B \in On) \to A \in On$
17		onsseleq	$⊢ (2_{𝑜} \in On \land A \in On) \to (2_{𝑜} \subseteq A \leftrightarrow (2_{𝑜} \in A \lor 2_{𝑜} = A))$
18	1 16 17	sylancr	$⊢ ((A \in On \land 1_{𝑜} \in A) \land B \in On) \to (2_{𝑜} \subseteq A \leftrightarrow (2_{𝑜} \in A \lor 2_{𝑜} = A))$
19		oewordri	$⊢ (A \in On \land B \in On) \to (2_{𝑜} \in A \to 2_{𝑜} ↑_{𝑜} B \subseteq A ↑_{𝑜} B)$
20	19	adantlr	$⊢ ((A \in On \land 1_{𝑜} \in A) \land B \in On) \to (2_{𝑜} \in A \to 2_{𝑜} ↑_{𝑜} B \subseteq A ↑_{𝑜} B)$
21		oveq1	$⊢ 2_{𝑜} = A \to 2_{𝑜} ↑_{𝑜} B = A ↑_{𝑜} B$
22		ssid	$⊢ A ↑_{𝑜} B \subseteq A ↑_{𝑜} B$
23	21 22	eqsstrdi	$⊢ 2_{𝑜} = A \to 2_{𝑜} ↑_{𝑜} B \subseteq A ↑_{𝑜} B$
24	23	a1i	$⊢ ((A \in On \land 1_{𝑜} \in A) \land B \in On) \to (2_{𝑜} = A \to 2_{𝑜} ↑_{𝑜} B \subseteq A ↑_{𝑜} B)$
25	20 24	jaod	$⊢ ((A \in On \land 1_{𝑜} \in A) \land B \in On) \to ((2_{𝑜} \in A \lor 2_{𝑜} = A) \to 2_{𝑜} ↑_{𝑜} B \subseteq A ↑_{𝑜} B)$
26	18 25	sylbid	$⊢ ((A \in On \land 1_{𝑜} \in A) \land B \in On) \to (2_{𝑜} \subseteq A \to 2_{𝑜} ↑_{𝑜} B \subseteq A ↑_{𝑜} B)$
27	15 26	mpd	$⊢ ((A \in On \land 1_{𝑜} \in A) \land B \in On) \to 2_{𝑜} ↑_{𝑜} B \subseteq A ↑_{𝑜} B$
28	10 27	sstrd	$⊢ ((A \in On \land 1_{𝑜} \in A) \land B \in On) \to B \subseteq A ↑_{𝑜} B$

Metamath Proof Explorer

Theorem oege2

Proof