This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wdomen1

Description: Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015)

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

Proof

Step Hyp Ref Expression
1 ensym 
 |-  ( A ~~ B -> B ~~ A )
2 endom 
 |-  ( B ~~ A -> B ~<_ A )
3 domwdom 
 |-  ( B ~<_ A -> B ~<_* A )
4 1 2 3 3syl 
 |-  ( A ~~ B -> B ~<_* A )
5 wdomtr 
 |-  ( ( B ~<_* A /\ A ~<_* C ) -> B ~<_* C )
6 4 5 sylan 
 |-  ( ( A ~~ B /\ A ~<_* C ) -> B ~<_* C )
7 endom 
 |-  ( A ~~ B -> A ~<_ B )
8 domwdom 
 |-  ( A ~<_ B -> A ~<_* B )
9 7 8 syl 
 |-  ( A ~~ B -> A ~<_* B )
10 wdomtr 
 |-  ( ( A ~<_* B /\ B ~<_* C ) -> A ~<_* C )
11 9 10 sylan 
 |-  ( ( A ~~ B /\ B ~<_* C ) -> A ~<_* C )
12 6 11 impbida 
 |-  ( A ~~ B -> ( A ~<_* C <-> B ~<_* C ) )