Metamath Proof Explorer

Theorem onssneli

Description: An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994)

Ref Expression
Hypothesis on.1 
|- A e. On
Assertion onssneli 
|- ( A C_ B -> -. B e. A )

Proof

Step Hyp Ref Expression
1 on.1 
 |-  A e. On
2 ssel 
 |-  ( A C_ B -> ( B e. A -> B e. B ) )
3 1 oneli 
 |-  ( B e. A -> B e. On )
4 eloni 
 |-  ( B e. On -> Ord B )
5 ordirr 
 |-  ( Ord B -> -. B e. B )
6 3 4 5 3syl 
 |-  ( B e. A -> -. B e. B )
7 2 6 nsyli 
 |-  ( A C_ B -> ( B e. A -> -. B e. A ) )
8 7 pm2.01d 
 |-  ( A C_ B -> -. B e. A )