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

Metamath Proof Explorer

Theorem ssntr

Description: An open subset of a set is a subset of the set's interior. (Contributed by Jeff Hankins, 31-Aug-2009) (Revised by Mario Carneiro, 11-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2		elin	$⊢ O \in (J \cap 𝒫 S) \leftrightarrow (O \in J \land O \in 𝒫 S)$
3		elpwg	$⊢ O \in J \to (O \in 𝒫 S \leftrightarrow O \subseteq S)$
4	3	pm5.32i	$⊢ (O \in J \land O \in 𝒫 S) \leftrightarrow (O \in J \land O \subseteq S)$
5	2 4	bitr2i	$⊢ (O \in J \land O \subseteq S) \leftrightarrow O \in (J \cap 𝒫 S)$
6		elssuni	$⊢ O \in (J \cap 𝒫 S) \to O \subseteq ⋃ (J \cap 𝒫 S)$
7	5 6	sylbi	$⊢ (O \in J \land O \subseteq S) \to O \subseteq ⋃ (J \cap 𝒫 S)$
8	7	adantl	$⊢ ((J \in Top \land S \subseteq X) \land (O \in J \land O \subseteq S)) \to O \subseteq ⋃ (J \cap 𝒫 S)$
9	1	ntrval	$⊢ (J \in Top \land S \subseteq X) \to int (J) (S) = ⋃ (J \cap 𝒫 S)$
10	9	adantr	$⊢ ((J \in Top \land S \subseteq X) \land (O \in J \land O \subseteq S)) \to int (J) (S) = ⋃ (J \cap 𝒫 S)$
11	8 10	sseqtrrd	$⊢ ((J \in Top \land S \subseteq X) \land (O \in J \land O \subseteq S)) \to O \subseteq int (J) (S)$