Theorem wdomen2

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

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

Proof

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