mrcss

Description: Closure preserves subset ordering. (Contributed by Stefan O'Rear, 31-Jan-2015)

		Ref	Expression
	Hypothesis	mrcfval.f	$⊢ F = mrCls (C)$
	Assertion	mrcss	$⊢ (C \in Moore (X) \land U \subseteq V \land V \subseteq X) \to F (U) \subseteq F (V)$

Step	Hyp	Ref	Expression
1		mrcfval.f	$⊢ F = mrCls (C)$
2		sstr2	$⊢ U \subseteq V \to (V \subseteq s \to U \subseteq s)$
3	2	adantr	$⊢ (U \subseteq V \land s \in C) \to (V \subseteq s \to U \subseteq s)$
4	3	ss2rabdv	$⊢ U \subseteq V \to \{s \in C \| V \subseteq s\} \subseteq \{s \in C \| U \subseteq s\}$
5		intss	$⊢ \{s \in C \| V \subseteq s\} \subseteq \{s \in C \| U \subseteq s\} \to ⋂ \{s \in C \| U \subseteq s\} \subseteq ⋂ \{s \in C \| V \subseteq s\}$
6	4 5	syl	$⊢ U \subseteq V \to ⋂ \{s \in C \| U \subseteq s\} \subseteq ⋂ \{s \in C \| V \subseteq s\}$
7	6	3ad2ant2	$⊢ (C \in Moore (X) \land U \subseteq V \land V \subseteq X) \to ⋂ \{s \in C \| U \subseteq s\} \subseteq ⋂ \{s \in C \| V \subseteq s\}$
8		simp1	$⊢ (C \in Moore (X) \land U \subseteq V \land V \subseteq X) \to C \in Moore (X)$
9		sstr	$⊢ (U \subseteq V \land V \subseteq X) \to U \subseteq X$
10	9	3adant1	$⊢ (C \in Moore (X) \land U \subseteq V \land V \subseteq X) \to U \subseteq X$
11	1	mrcval	$⊢ (C \in Moore (X) \land U \subseteq X) \to F (U) = ⋂ \{s \in C \| U \subseteq s\}$
12	8 10 11	syl2anc	$⊢ (C \in Moore (X) \land U \subseteq V \land V \subseteq X) \to F (U) = ⋂ \{s \in C \| U \subseteq s\}$
13	1	mrcval	$⊢ (C \in Moore (X) \land V \subseteq X) \to F (V) = ⋂ \{s \in C \| V \subseteq s\}$
14	13	3adant2	$⊢ (C \in Moore (X) \land U \subseteq V \land V \subseteq X) \to F (V) = ⋂ \{s \in C \| V \subseteq s\}$
15	7 12 14	3sstr4d	$⊢ (C \in Moore (X) \land U \subseteq V \land V \subseteq X) \to F (U) \subseteq F (V)$

Metamath Proof Explorer