Theorem onsucwordi

Description: The successor operation preserves the less-than-or-equal relationship between ordinals. Lemma 3.1 of Schloeder p. 7. (Contributed by RP, 29-Jan-2025)

	Ref	Expression
Assertion	onsucwordi	|- ( ( A e. On /\ B e. On ) -> ( A C_ B -> suc A C_ suc B ) )

Proof

Step	Hyp	Ref	Expression
1		eloni	|- ( A e. On -> Ord A )
2		eloni	|- ( B e. On -> Ord B )
3		ordsucsssuc	|- ( ( Ord A /\ Ord B ) -> ( A C_ B <-> suc A C_ suc B ) )
4	1 2 3	syl2an	|- ( ( A e. On /\ B e. On ) -> ( A C_ B <-> suc A C_ suc B ) )
5	4	biimpd	|- ( ( A e. On /\ B e. On ) -> ( A C_ B -> suc A C_ suc B ) )