Theorem wdomen2

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

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

Proof

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