oeord2lim

Description: Given a limit ordinal, the power of any base at least as large as two raised to an ordinal less than that limit ordinal is less than the power of that base raised to the limit ordinal . Lemma 3.22 of Schloeder p. 10. See oeordi . (Contributed by RP, 30-Jan-2025)

		Ref	Expression
	Assertion	oeord2lim	$⊢ ((A \in On \land 1_{𝑜} \in A) \land (Lim C \land C \in V)) \to (B \in C \to A ↑_{𝑜} B \in (A ↑_{𝑜} C))$

Proof

Step	Hyp	Ref	Expression
1		limelon	$⊢ (C \in V \land Lim C) \to C \in On$
2	1	ancoms	$⊢ (Lim C \land C \in V) \to C \in On$
3		ondif2	$⊢ A \in (On ∖ 2_{𝑜}) \leftrightarrow (A \in On \land 1_{𝑜} \in A)$
4	3	biimpri	$⊢ (A \in On \land 1_{𝑜} \in A) \to A \in (On ∖ 2_{𝑜})$
5		oeordi	$⊢ (C \in On \land A \in (On ∖ 2_{𝑜})) \to (B \in C \to A ↑_{𝑜} B \in (A ↑_{𝑜} C))$
6	2 4 5	syl2anr	$⊢ ((A \in On \land 1_{𝑜} \in A) \land (Lim C \land C \in V)) \to (B \in C \to A ↑_{𝑜} B \in (A ↑_{𝑜} C))$

Metamath Proof Explorer

Theorem oeord2lim

Proof