Metamath Proof Explorer

Theorem ntrss

Description: Subset relationship for interior. (Contributed by NM, 3-Oct-2007)

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

Proof

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2		sscon	$⊢ T \subseteq S \to X ∖ S \subseteq X ∖ T$
3	2	adantl	$⊢ (S \subseteq X \land T \subseteq S) \to X ∖ S \subseteq X ∖ T$
4		difss	$⊢ X ∖ T \subseteq X$
5	3 4	jctil	$⊢ (S \subseteq X \land T \subseteq S) \to (X ∖ T \subseteq X \land X ∖ S \subseteq X ∖ T)$
6	1	clsss	$⊢ (J \in Top \land X ∖ T \subseteq X \land X ∖ S \subseteq X ∖ T) \to cls (J) (X ∖ S) \subseteq cls (J) (X ∖ T)$
7	6	3expb	$⊢ (J \in Top \land (X ∖ T \subseteq X \land X ∖ S \subseteq X ∖ T)) \to cls (J) (X ∖ S) \subseteq cls (J) (X ∖ T)$
8	5 7	sylan2	$⊢ (J \in Top \land (S \subseteq X \land T \subseteq S)) \to cls (J) (X ∖ S) \subseteq cls (J) (X ∖ T)$
9	8	sscond	$⊢ (J \in Top \land (S \subseteq X \land T \subseteq S)) \to X ∖ cls (J) (X ∖ T) \subseteq X ∖ cls (J) (X ∖ S)$
10		sstr2	$⊢ T \subseteq S \to (S \subseteq X \to T \subseteq X)$
11	10	impcom	$⊢ (S \subseteq X \land T \subseteq S) \to T \subseteq X$
12	1	ntrval2	$⊢ (J \in Top \land T \subseteq X) \to int (J) (T) = X ∖ cls (J) (X ∖ T)$
13	11 12	sylan2	$⊢ (J \in Top \land (S \subseteq X \land T \subseteq S)) \to int (J) (T) = X ∖ cls (J) (X ∖ T)$
14	1	ntrval2	$⊢ (J \in Top \land S \subseteq X) \to int (J) (S) = X ∖ cls (J) (X ∖ S)$
15	14	adantrr	$⊢ (J \in Top \land (S \subseteq X \land T \subseteq S)) \to int (J) (S) = X ∖ cls (J) (X ∖ S)$
16	9 13 15	3sstr4d	$⊢ (J \in Top \land (S \subseteq X \land T \subseteq S)) \to int (J) (T) \subseteq int (J) (S)$
17	16	3impb	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to int (J) (T) \subseteq int (J) (S)$