Theorem mapdcnv11N

Description: The converse of the map defined by df-mapd is one-to-one. (Contributed by NM, 13-Mar-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapdcnvord.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdcnvord.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdcnvord.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdcnvord.x	$$⊢\phi \to X\in \mathrm{ran}M$$
	mapdcnvord.y	$$⊢\phi \to Y\in \mathrm{ran}M$$
Assertion	mapdcnv11N	$$⊢\phi \to \left(M^{-1}\left(X\right)=M^{-1}\left(Y\right)\leftrightarrow X=Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		mapdcnvord.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdcnvord.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
3		mapdcnvord.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
4		mapdcnvord.x	$$⊢\phi \to X\in \mathrm{ran}M$$
5		mapdcnvord.y	$$⊢\phi \to Y\in \mathrm{ran}M$$
6	1 2 3 4 5	mapdcnvordN	$$⊢\phi \to \left(M^{-1}\left(X\right)\subseteq M^{-1}\left(Y\right)\leftrightarrow X\subseteq Y\right)$$
7	1 2 3 5 4	mapdcnvordN	$$⊢\phi \to \left(M^{-1}\left(Y\right)\subseteq M^{-1}\left(X\right)\leftrightarrow Y\subseteq X\right)$$
8	6 7	anbi12d	$$⊢\phi \to \left(\left(M^{-1}\left(X\right)\subseteq M^{-1}\left(Y\right)\wedge M^{-1}\left(Y\right)\subseteq M^{-1}\left(X\right)\right)\leftrightarrow \left(X\subseteq Y\wedge Y\subseteq X\right)\right)$$
9		eqss	$$⊢M^{-1}\left(X\right)=M^{-1}\left(Y\right)\leftrightarrow \left(M^{-1}\left(X\right)\subseteq M^{-1}\left(Y\right)\wedge M^{-1}\left(Y\right)\subseteq M^{-1}\left(X\right)\right)$$
10		eqss	$$⊢X=Y\leftrightarrow \left(X\subseteq Y\wedge Y\subseteq X\right)$$
11	8 9 10	3bitr4g	$$⊢\phi \to \left(M^{-1}\left(X\right)=M^{-1}\left(Y\right)\leftrightarrow X=Y\right)$$