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	$$⊢A\in \mathrm{On}\to \left(B\in A\to \mathrm{suc}B\subseteq A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eloni	$$⊢A\in \mathrm{On}\to \mathrm{Ord}A$$
2		ordsucss	$$⊢\mathrm{Ord}A\to \left(B\in A\to \mathrm{suc}B\subseteq A\right)$$
3	1 2	syl	$$⊢A\in \mathrm{On}\to \left(B\in A\to \mathrm{suc}B\subseteq A\right)$$