Theorem sdomel

Description: For ordinals, strict dominance implies membership. (Contributed by Mario Carneiro, 13-Jan-2013)

	Ref	Expression
Assertion	sdomel	|- ( ( A e. On /\ B e. On ) -> ( A ~< B -> A e. B ) )

Proof

Step	Hyp	Ref	Expression
1		ssdomg	|- ( A e. On -> ( B C_ A -> B ~<_ A ) )
2	1	adantl	|- ( ( B e. On /\ A e. On ) -> ( B C_ A -> B ~<_ A ) )
3		ontri1	|- ( ( B e. On /\ A e. On ) -> ( B C_ A <-> -. A e. B ) )
4		domtriord	|- ( ( B e. On /\ A e. On ) -> ( B ~<_ A <-> -. A ~< B ) )
5	2 3 4	3imtr3d	|- ( ( B e. On /\ A e. On ) -> ( -. A e. B -> -. A ~< B ) )
6	5	con4d	|- ( ( B e. On /\ A e. On ) -> ( A ~< B -> A e. B ) )
7	6	ancoms	|- ( ( A e. On /\ B e. On ) -> ( A ~< B -> A e. B ) )