Metamath Proof Explorer

Theorem sdomen2

Description: Equality-like theorem for equinumerosity and strict dominance. (Contributed by NM, 8-Nov-2003)

Ref Expression
Assertion sdomen2 
|- ( A ~~ B -> ( C ~< A <-> C ~< B ) )

Proof

Step Hyp Ref Expression
1 sdomentr 
 |-  ( ( C ~< A /\ A ~~ B ) -> C ~< B )
2 1 ancoms 
 |-  ( ( A ~~ B /\ C ~< A ) -> C ~< B )
3 ensym 
 |-  ( A ~~ B -> B ~~ A )
4 sdomentr 
 |-  ( ( C ~< B /\ B ~~ A ) -> C ~< A )
5 4 ancoms 
 |-  ( ( B ~~ A /\ C ~< B ) -> C ~< A )
6 3 5 sylan 
 |-  ( ( A ~~ B /\ C ~< B ) -> C ~< A )
7 2 6 impbida 
 |-  ( A ~~ B -> ( C ~< A <-> C ~< B ) )