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 )