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 ∈ On ∧ 1 𝑜 ∈ A ∧ B ∈ On ∧ C ∈ On → B ∈ C ↔ A ↑ 𝑜 B ∈ A ↑ 𝑜 C

Proof

Step Hyp Ref Expression
1 ondif2 ⊢ A ∈ On ∖ 2 𝑜 ↔ A ∈ On ∧ 1 𝑜 ∈ A
2 1 3anbi1i ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ↔ A ∈ On ∧ 1 𝑜 ∈ A ∧ B ∈ On ∧ C ∈ On
3 3anrot ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ↔ B ∈ On ∧ C ∈ On ∧ A ∈ On ∖ 2 𝑜
4 2 3 sylbb1 ⊢ A ∈ On ∧ 1 𝑜 ∈ A ∧ B ∈ On ∧ C ∈ On → B ∈ On ∧ C ∈ On ∧ A ∈ On ∖ 2 𝑜
5 oeord ⊢ B ∈ On ∧ C ∈ On ∧ A ∈ On ∖ 2 𝑜 → B ∈ C ↔ A ↑ 𝑜 B ∈ A ↑ 𝑜 C
6 4 5 syl ⊢ A ∈ On ∧ 1 𝑜 ∈ A ∧ B ∈ On ∧ C ∈ On → B ∈ C ↔ A ↑ 𝑜 B ∈ A ↑ 𝑜 C