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 e. On -> E. x e. On A e. x )

Proof

Step Hyp Ref Expression
1 onsuc 
 |-  ( A e. On -> suc A e. On )
2 sucidg 
 |-  ( A e. On -> A e. suc A )
3 eleq2 
 |-  ( x = suc A -> ( A e. x <-> A e. suc A ) )
4 3 rspcev 
 |-  ( ( suc A e. On /\ A e. suc A ) -> E. x e. On A e. x )
5 1 2 4 syl2anc 
 |-  ( A e. On -> E. x e. On A e. x )