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	⊢ ( ( ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ∈ 𝐶 ↔ ( 𝐴 ↑o 𝐵 ) ∈ ( 𝐴 ↑o 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ondif2	⊢ ( 𝐴 ∈ ( On ∖ 2o ) ↔ ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) )
2	1	3anbi1i	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ↔ ( ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) )
3		3anrot	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ↔ ( 𝐵 ∈ On ∧ 𝐶 ∈ On ∧ 𝐴 ∈ ( On ∖ 2o ) ) )
4	2 3	sylbb1	⊢ ( ( ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ∈ On ∧ 𝐶 ∈ On ∧ 𝐴 ∈ ( On ∖ 2o ) ) )
5		oeord	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ∧ 𝐴 ∈ ( On ∖ 2o ) ) → ( 𝐵 ∈ 𝐶 ↔ ( 𝐴 ↑o 𝐵 ) ∈ ( 𝐴 ↑o 𝐶 ) ) )
6	4 5	syl	⊢ ( ( ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ∈ 𝐶 ↔ ( 𝐴 ↑o 𝐵 ) ∈ ( 𝐴 ↑o 𝐶 ) ) )