This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem onnmin

Description: No member of a set of ordinal numbers belongs to its minimum. (Contributed by NM, 2-Feb-1997)

Ref Expression
Assertion onnmin 
|- ( ( A C_ On /\ B e. A ) -> -. B e. |^| A )

Proof

Step Hyp Ref Expression
1 intss1 
 |-  ( B e. A -> |^| A C_ B )
2 1 adantl 
 |-  ( ( A C_ On /\ B e. A ) -> |^| A C_ B )
3 ne0i 
 |-  ( B e. A -> A =/= (/) )
4 oninton 
 |-  ( ( A C_ On /\ A =/= (/) ) -> |^| A e. On )
5 3 4 sylan2 
 |-  ( ( A C_ On /\ B e. A ) -> |^| A e. On )
6 ssel2 
 |-  ( ( A C_ On /\ B e. A ) -> B e. On )
7 ontri1 
 |-  ( ( |^| A e. On /\ B e. On ) -> ( |^| A C_ B <-> -. B e. |^| A ) )
8 5 6 7 syl2anc 
 |-  ( ( A C_ On /\ B e. A ) -> ( |^| A C_ B <-> -. B e. |^| A ) )
9 2 8 mpbid 
 |-  ( ( A C_ On /\ B e. A ) -> -. B e. |^| A )