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 e. On -> A _E suc A )

Proof

Step Hyp Ref Expression
1 sucidg 
 |-  ( A e. On -> A e. suc A )
2 onsuc 
 |-  ( A e. On -> suc A e. On )
3 epelg 
 |-  ( suc A e. On -> ( A _E suc A <-> A e. suc A ) )
4 2 3 syl 
 |-  ( A e. On -> ( A _E suc A <-> A e. suc A ) )
5 1 4 mpbird 
 |-  ( A e. On -> A _E suc A )