Metamath Proof Explorer

Theorem oeord2com

Description: When the same base at least as large as two is raised to ordinal powers, , ordering of the power is equivalent to the ordering of the exponents. Theorem 3.24 of Schloeder p. 11. (Contributed by RP, 30-Jan-2025)

		Ref	Expression
	Assertion	oeord2com	$⊢ ((A \in On \land 1_{𝑜} \in A) \land B \in On \land C \in On) \to (B \in C \leftrightarrow 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	3anbi1i	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in On \land C \in On) \leftrightarrow ((A \in On \land 1_{𝑜} \in A) \land B \in On \land C \in On)$
3		3anrot	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in On \land C \in On) \leftrightarrow (B \in On \land C \in On \land A \in (On ∖ 2_{𝑜}))$
4	2 3	sylbb1	$⊢ ((A \in On \land 1_{𝑜} \in A) \land B \in On \land C \in On) \to (B \in On \land C \in On \land A \in (On ∖ 2_{𝑜}))$
5		oeord	$⊢ (B \in On \land C \in On \land A \in (On ∖ 2_{𝑜})) \to (B \in C \leftrightarrow A ↑_{𝑜} B \in (A ↑_{𝑜} C))$
6	4 5	syl	$⊢ ((A \in On \land 1_{𝑜} \in A) \land B \in On \land C \in On) \to (B \in C \leftrightarrow A ↑_{𝑜} B \in (A ↑_{𝑜} C))$