Metamath Proof Explorer


Theorem domen2

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

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

Proof

Step Hyp Ref Expression
1 domentr
 |-  ( ( C ~<_ A /\ A ~~ B ) -> C ~<_ B )
2 1 ancoms
 |-  ( ( A ~~ B /\ C ~<_ A ) -> C ~<_ B )
3 ensym
 |-  ( A ~~ B -> B ~~ A )
4 domentr
 |-  ( ( 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 ) )