Metamath Proof Explorer

Theorem lspss

Description: Span preserves subset ordering. ( spanss analog.) (Contributed by NM, 11-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

		Ref	Expression
	Hypotheses	lspss.v	$⊢ V = {Base}_{W}$
		lspss.n	$⊢ N = LSpan (W)$
	Assertion	lspss	$⊢ (W \in LMod \land U \subseteq V \land T \subseteq U) \to N (T) \subseteq N (U)$

Proof

Step	Hyp	Ref	Expression
1		lspss.v	$⊢ V = {Base}_{W}$
2		lspss.n	$⊢ N = LSpan (W)$
3		simpl3	$⊢ ((W \in LMod \land U \subseteq V \land T \subseteq U) \land t \in LSubSp (W)) \to T \subseteq U$
4		sstr2	$⊢ T \subseteq U \to (U \subseteq t \to T \subseteq t)$
5	3 4	syl	$⊢ ((W \in LMod \land U \subseteq V \land T \subseteq U) \land t \in LSubSp (W)) \to (U \subseteq t \to T \subseteq t)$
6	5	ss2rabdv	$⊢ (W \in LMod \land U \subseteq V \land T \subseteq U) \to \{t \in LSubSp (W) \| U \subseteq t\} \subseteq \{t \in LSubSp (W) \| T \subseteq t\}$
7		intss	$⊢ \{t \in LSubSp (W) \| U \subseteq t\} \subseteq \{t \in LSubSp (W) \| T \subseteq t\} \to ⋂ \{t \in LSubSp (W) \| T \subseteq t\} \subseteq ⋂ \{t \in LSubSp (W) \| U \subseteq t\}$
8	6 7	syl	$⊢ (W \in LMod \land U \subseteq V \land T \subseteq U) \to ⋂ \{t \in LSubSp (W) \| T \subseteq t\} \subseteq ⋂ \{t \in LSubSp (W) \| U \subseteq t\}$
9		simp1	$⊢ (W \in LMod \land U \subseteq V \land T \subseteq U) \to W \in LMod$
10		simp3	$⊢ (W \in LMod \land U \subseteq V \land T \subseteq U) \to T \subseteq U$
11		simp2	$⊢ (W \in LMod \land U \subseteq V \land T \subseteq U) \to U \subseteq V$
12	10 11	sstrd	$⊢ (W \in LMod \land U \subseteq V \land T \subseteq U) \to T \subseteq V$
13		eqid	$⊢ LSubSp (W) = LSubSp (W)$
14	1 13 2	lspval	$⊢ (W \in LMod \land T \subseteq V) \to N (T) = ⋂ \{t \in LSubSp (W) \| T \subseteq t\}$
15	9 12 14	syl2anc	$⊢ (W \in LMod \land U \subseteq V \land T \subseteq U) \to N (T) = ⋂ \{t \in LSubSp (W) \| T \subseteq t\}$
16	1 13 2	lspval	$⊢ (W \in LMod \land U \subseteq V) \to N (U) = ⋂ \{t \in LSubSp (W) \| U \subseteq t\}$
17	16	3adant3	$⊢ (W \in LMod \land U \subseteq V \land T \subseteq U) \to N (U) = ⋂ \{t \in LSubSp (W) \| U \subseteq t\}$
18	8 15 17	3sstr4d	$⊢ (W \in LMod \land U \subseteq V \land T \subseteq U) \to N (T) \subseteq N (U)$