mapdcnvordN

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

	Ref	Expression
Hypotheses	mapdcnvord.h	$⊢ H = LHyp (K)$
	mapdcnvord.m	$⊢ M = mapd (K) (W)$
	mapdcnvord.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdcnvord.x	$⊢ φ \to X \in ran M$
	mapdcnvord.y	$⊢ φ \to Y \in ran M$
Assertion	mapdcnvordN	$⊢ φ \to (M^{-1} (X) \subseteq M^{-1} (Y) \leftrightarrow X \subseteq Y)$

Step	Hyp	Ref	Expression
1		mapdcnvord.h	$⊢ H = LHyp (K)$
2		mapdcnvord.m	$⊢ M = mapd (K) (W)$
3		mapdcnvord.k	$⊢ φ \to (K \in HL \land W \in H)$
4		mapdcnvord.x	$⊢ φ \to X \in ran M$
5		mapdcnvord.y	$⊢ φ \to Y \in ran M$
6		eqid	$⊢ DVecH (K) (W) = DVecH (K) (W)$
7		eqid	$⊢ LSubSp (DVecH (K) (W)) = LSubSp (DVecH (K) (W))$
8	1 2 6 7 3 4	mapdcnvcl	$⊢ φ \to M^{-1} (X) \in LSubSp (DVecH (K) (W))$
9	1 2 6 7 3 5	mapdcnvcl	$⊢ φ \to M^{-1} (Y) \in LSubSp (DVecH (K) (W))$
10	1 6 7 2 3 8 9	mapdord	$⊢ φ \to (M (M^{-1} (X)) \subseteq M (M^{-1} (Y)) \leftrightarrow M^{-1} (X) \subseteq M^{-1} (Y))$
11	1 2 3 4	mapdcnvid2	$⊢ φ \to M (M^{-1} (X)) = X$
12	1 2 3 5	mapdcnvid2	$⊢ φ \to M (M^{-1} (Y)) = Y$
13	11 12	sseq12d	$⊢ φ \to (M (M^{-1} (X)) \subseteq M (M^{-1} (Y)) \leftrightarrow X \subseteq Y)$
14	10 13	bitr3d	$⊢ φ \to (M^{-1} (X) \subseteq M^{-1} (Y) \leftrightarrow X \subseteq Y)$

Metamath Proof Explorer