oeord2i

Description: Ordinal exponentiation of the same base at least as large as two preserves the ordering of the exponents. Lemma 3.23 of Schloeder p. 11. (Contributed by RP, 30-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		ondif2	$⊢ A \in (On ∖ 2_{𝑜}) \leftrightarrow (A \in On \land 1_{𝑜} \in A)$
2	1	biimpri	$⊢ (A \in On \land 1_{𝑜} \in A) \to A \in (On ∖ 2_{𝑜})$
3	2	anim1ci	$⊢ ((A \in On \land 1_{𝑜} \in A) \land C \in On) \to (C \in On \land A \in (On ∖ 2_{𝑜}))$
4		oeordi	$⊢ (C \in On \land A \in (On ∖ 2_{𝑜})) \to (B \in C \to A ↑_{𝑜} B \in (A ↑_{𝑜} C))$
5	3 4	syl	$⊢ ((A \in On \land 1_{𝑜} \in A) \land C \in On) \to (B \in C \to A ↑_{𝑜} B \in (A ↑_{𝑜} C))$

Metamath Proof Explorer

Theorem oeord2i

Proof