Theorem wdomen1

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

	Ref	Expression
Assertion	wdomen1	$$⊢A\approx B\to \left(A{\preccurlyeq }^{*}C\leftrightarrow B{\preccurlyeq }^{*}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		ensym	$$⊢A\approx B\to B\approx A$$
2		endom	$$⊢B\approx A\to B\preccurlyeq A$$
3		domwdom	$$⊢B\preccurlyeq A\to B{\preccurlyeq }^{*}A$$
4	1 2 3	3syl	$$⊢A\approx B\to B{\preccurlyeq }^{*}A$$
5		wdomtr	$$⊢\left(B{\preccurlyeq }^{*}A\wedge A{\preccurlyeq }^{*}C\right)\to B{\preccurlyeq }^{*}C$$
6	4 5	sylan	$$⊢\left(A\approx B\wedge A{\preccurlyeq }^{*}C\right)\to B{\preccurlyeq }^{*}C$$
7		endom	$$⊢A\approx B\to A\preccurlyeq B$$
8		domwdom	$$⊢A\preccurlyeq B\to A{\preccurlyeq }^{*}B$$
9	7 8	syl	$$⊢A\approx B\to A{\preccurlyeq }^{*}B$$
10		wdomtr	$$⊢\left(A{\preccurlyeq }^{*}B\wedge B{\preccurlyeq }^{*}C\right)\to A{\preccurlyeq }^{*}C$$
11	9 10	sylan	$$⊢\left(A\approx B\wedge B{\preccurlyeq }^{*}C\right)\to A{\preccurlyeq }^{*}C$$
12	6 11	impbida	$$⊢A\approx B\to \left(A{\preccurlyeq }^{*}C\leftrightarrow B{\preccurlyeq }^{*}C\right)$$