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	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → suc 𝐴 ⊆ suc 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
2		eloni	⊢ ( 𝐵 ∈ On → Ord 𝐵 )
3		ordsucsssuc	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝐵 ) )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝐵 ) )
5	4	biimpd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → suc 𝐴 ⊆ suc 𝐵 ) )