Theorem onepsuc

Description: Every ordinal is less than its successor, relationship version. Lemma 1.7 of Schloeder p. 1. (Contributed by RP, 15-Jan-2025)

	Ref	Expression
Assertion	onepsuc	$$⊢A\in \mathrm{On}\to A\mathrm{E}\mathrm{suc}A$$

Proof

Step	Hyp	Ref	Expression
1		sucidg	$$⊢A\in \mathrm{On}\to A\in \mathrm{suc}A$$
2		onsuc	$$⊢A\in \mathrm{On}\to \mathrm{suc}A\in \mathrm{On}$$
3		epelg	$$⊢\mathrm{suc}A\in \mathrm{On}\to \left(A\mathrm{E}\mathrm{suc}A\leftrightarrow A\in \mathrm{suc}A\right)$$
4	2 3	syl	$$⊢A\in \mathrm{On}\to \left(A\mathrm{E}\mathrm{suc}A\leftrightarrow A\in \mathrm{suc}A\right)$$
5	1 4	mpbird	$$⊢A\in \mathrm{On}\to A\mathrm{E}\mathrm{suc}A$$