Metamath Proof Explorer

Theorem onexgt

Description: For any ordinal, there is always a larger ordinal. (Contributed by RP, 1-Feb-2025)

		Ref	Expression
	Assertion	onexgt	$⊢ A \in On \to \exists x \in On A \in x$

Step	Hyp	Ref	Expression
1		onsuc	$⊢ A \in On \to suc A \in On$
2		sucidg	$⊢ A \in On \to A \in suc A$
3		eleq2	$⊢ x = suc A \to (A \in x \leftrightarrow A \in suc A)$
4	3	rspcev	$⊢ (suc A \in On \land A \in suc A) \to \exists x \in On A \in x$
5	1 2 4	syl2anc	$⊢ A \in On \to \exists x \in On A \in x$