Theorem onsucss

Description: If one ordinal is less than another, then the successor of the first is less than or equal to the second. Lemma 1.13 of Schloeder p. 2. See ordsucss . (Contributed by RP, 16-Jan-2025)

	Ref	Expression
Assertion	onsucss	⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
2		ordsucss	⊢ ( Ord 𝐴 → ( 𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴 ) )
3	1 2	syl	⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴 ) )