Metamath Proof Explorer

Theorem onpsssuc

Description: An ordinal number is a proper subset of its successor. (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Assertion onpsssuc 
|- ( A e. On -> A C. suc A )

Proof

Step Hyp Ref Expression
1 sucidg 
 |-  ( A e. On -> A e. suc A )
2 eloni 
 |-  ( A e. On -> Ord A )
3 ordsuc 
 |-  ( Ord A <-> Ord suc A )
4 2 3 sylib 
 |-  ( A e. On -> Ord suc A )
5 ordelpss 
 |-  ( ( Ord A /\ Ord suc A ) -> ( A e. suc A <-> A C. suc A ) )
6 2 4 5 syl2anc 
 |-  ( A e. On -> ( A e. suc A <-> A C. suc A ) )
7 1 6 mpbid 
 |-  ( A e. On -> A C. suc A )