mapdsord

Description: Strong ordering property of themap defined by df-mapd . (Contributed by NM, 13-Mar-2015)

	Ref	Expression
Hypotheses	mapdcnvcl.h	$⊢ H = LHyp (K)$
	mapdcnvcl.m	$⊢ M = mapd (K) (W)$
	mapdcnvcl.u	$⊢ U = DVecH (K) (W)$
	mapdcnvcl.s	$⊢ S = LSubSp (U)$
	mapdcnvcl.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdcl.x	$⊢ φ \to X \in S$
	mapdsord.x	$⊢ φ \to Y \in S$
Assertion	mapdsord	$⊢ φ \to (M (X) \subset M (Y) \leftrightarrow X \subset Y)$

Step	Hyp	Ref	Expression
1		mapdcnvcl.h	$⊢ H = LHyp (K)$
2		mapdcnvcl.m	$⊢ M = mapd (K) (W)$
3		mapdcnvcl.u	$⊢ U = DVecH (K) (W)$
4		mapdcnvcl.s	$⊢ S = LSubSp (U)$
5		mapdcnvcl.k	$⊢ φ \to (K \in HL \land W \in H)$
6		mapdcl.x	$⊢ φ \to X \in S$
7		mapdsord.x	$⊢ φ \to Y \in S$
8	1 3 4 2 5 6 7	mapdord	$⊢ φ \to (M (X) \subseteq M (Y) \leftrightarrow X \subseteq Y)$
9	1 3 4 2 5 6 7	mapd11	$⊢ φ \to (M (X) = M (Y) \leftrightarrow X = Y)$
10	9	necon3bid	$⊢ φ \to (M (X) \neq M (Y) \leftrightarrow X \neq Y)$
11	8 10	anbi12d	$⊢ φ \to ((M (X) \subseteq M (Y) \land M (X) \neq M (Y)) \leftrightarrow (X \subseteq Y \land X \neq Y))$
12		df-pss	$⊢ M (X) \subset M (Y) \leftrightarrow (M (X) \subseteq M (Y) \land M (X) \neq M (Y))$
13		df-pss	$⊢ X \subset Y \leftrightarrow (X \subseteq Y \land X \neq Y)$
14	11 12 13	3bitr4g	$⊢ φ \to (M (X) \subset M (Y) \leftrightarrow X \subset Y)$

Metamath Proof Explorer