Description: Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | domen2 | |- ( A ~~ B -> ( C ~<_ A <-> C ~<_ B ) ) |
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 ) ) |