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

Proof

Step	Hyp	Ref	Expression
1		ondif2	⊢ ( 𝐴 ∈ ( On ∖ 2o ) ↔ ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) )
2	1	biimpri	⊢ ( ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) → 𝐴 ∈ ( On ∖ 2o ) )
3	2	anim1ci	⊢ ( ( ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) ∧ 𝐶 ∈ On ) → ( 𝐶 ∈ On ∧ 𝐴 ∈ ( On ∖ 2o ) ) )
4		oeordi	⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ ( On ∖ 2o ) ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 ↑o 𝐵 ) ∈ ( 𝐴 ↑o 𝐶 ) ) )
5	3 4	syl	⊢ ( ( ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) ∧ 𝐶 ∈ On ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 ↑o 𝐵 ) ∈ ( 𝐴 ↑o 𝐶 ) ) )