This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clsss

Description: Subset relationship for closure. (Contributed by NM, 10-Feb-2007)

		Ref	Expression
	Hypothesis	clscld.1	$⊢ X = ⋃ J$
	Assertion	clsss	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to cls (J) (T) \subseteq cls (J) (S)$

Proof

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2		sstr2	$⊢ T \subseteq S \to (S \subseteq x \to T \subseteq x)$
3	2	adantr	$⊢ (T \subseteq S \land x \in Clsd (J)) \to (S \subseteq x \to T \subseteq x)$
4	3	ss2rabdv	$⊢ T \subseteq S \to \{x \in Clsd (J) \| S \subseteq x\} \subseteq \{x \in Clsd (J) \| T \subseteq x\}$
5		intss	$⊢ \{x \in Clsd (J) \| S \subseteq x\} \subseteq \{x \in Clsd (J) \| T \subseteq x\} \to ⋂ \{x \in Clsd (J) \| T \subseteq x\} \subseteq ⋂ \{x \in Clsd (J) \| S \subseteq x\}$
6	4 5	syl	$⊢ T \subseteq S \to ⋂ \{x \in Clsd (J) \| T \subseteq x\} \subseteq ⋂ \{x \in Clsd (J) \| S \subseteq x\}$
7	6	3ad2ant3	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to ⋂ \{x \in Clsd (J) \| T \subseteq x\} \subseteq ⋂ \{x \in Clsd (J) \| S \subseteq x\}$
8		simp1	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to J \in Top$
9		sstr2	$⊢ T \subseteq S \to (S \subseteq X \to T \subseteq X)$
10	9	impcom	$⊢ (S \subseteq X \land T \subseteq S) \to T \subseteq X$
11	10	3adant1	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to T \subseteq X$
12	1	clsval	$⊢ (J \in Top \land T \subseteq X) \to cls (J) (T) = ⋂ \{x \in Clsd (J) \| T \subseteq x\}$
13	8 11 12	syl2anc	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to cls (J) (T) = ⋂ \{x \in Clsd (J) \| T \subseteq x\}$
14	1	clsval	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) = ⋂ \{x \in Clsd (J) \| S \subseteq x\}$
15	14	3adant3	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to cls (J) (S) = ⋂ \{x \in Clsd (J) \| S \subseteq x\}$
16	7 13 15	3sstr4d	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to cls (J) (T) \subseteq cls (J) (S)$