Metamath Proof Explorer

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 On \to A E suc A$

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