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 e. On /\ 1o e. A ) /\ B e. On /\ C e. On ) -> ( B e. C <-> ( A ^o B ) e. ( A ^o C ) ) )

Proof

Step	Hyp	Ref	Expression
1		ondif2	|- ( A e. ( On \ 2o ) <-> ( A e. On /\ 1o e. A ) )
2	1	3anbi1i	|- ( ( A e. ( On \ 2o ) /\ B e. On /\ C e. On ) <-> ( ( A e. On /\ 1o e. A ) /\ B e. On /\ C e. On ) )
3		3anrot	|- ( ( A e. ( On \ 2o ) /\ B e. On /\ C e. On ) <-> ( B e. On /\ C e. On /\ A e. ( On \ 2o ) ) )
4	2 3	sylbb1	|- ( ( ( A e. On /\ 1o e. A ) /\ B e. On /\ C e. On ) -> ( B e. On /\ C e. On /\ A e. ( On \ 2o ) ) )
5		oeord	|- ( ( B e. On /\ C e. On /\ A e. ( On \ 2o ) ) -> ( B e. C <-> ( A ^o B ) e. ( A ^o C ) ) )
6	4 5	syl	|- ( ( ( A e. On /\ 1o e. A ) /\ B e. On /\ C e. On ) -> ( B e. C <-> ( A ^o B ) e. ( A ^o C ) ) )