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 ) )