Metamath Proof Explorer

Theorem ntrval

Description: The interior of a subset of a topology's base set is the union of all the open sets it includes. Definition of interior of Munkres p. 94. (Contributed by NM, 10-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013)

		Ref	Expression
	Hypothesis	iscld.1	$⊢ X = ⋃ J$
	Assertion	ntrval	$⊢ (J \in Top \land S \subseteq X) \to int (J) (S) = ⋃ (J \cap 𝒫 S)$

Proof

Step	Hyp	Ref	Expression
1		iscld.1	$⊢ X = ⋃ J$
2	1	ntrfval	$⊢ J \in Top \to int (J) = (x \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 x))$
3	2	fveq1d	$⊢ J \in Top \to int (J) (S) = (x \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 x)) (S)$
4	3	adantr	$⊢ (J \in Top \land S \subseteq X) \to int (J) (S) = (x \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 x)) (S)$
5		eqid	$⊢ (x \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 x)) = (x \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 x))$
6		pweq	$⊢ x = S \to 𝒫 x = 𝒫 S$
7	6	ineq2d	$⊢ x = S \to J \cap 𝒫 x = J \cap 𝒫 S$
8	7	unieqd	$⊢ x = S \to ⋃ (J \cap 𝒫 x) = ⋃ (J \cap 𝒫 S)$
9	1	topopn	$⊢ J \in Top \to X \in J$
10		elpw2g	$⊢ X \in J \to (S \in 𝒫 X \leftrightarrow S \subseteq X)$
11	9 10	syl	$⊢ J \in Top \to (S \in 𝒫 X \leftrightarrow S \subseteq X)$
12	11	biimpar	$⊢ (J \in Top \land S \subseteq X) \to S \in 𝒫 X$
13		inex1g	$⊢ J \in Top \to J \cap 𝒫 S \in V$
14	13	adantr	$⊢ (J \in Top \land S \subseteq X) \to J \cap 𝒫 S \in V$
15	14	uniexd	$⊢ (J \in Top \land S \subseteq X) \to ⋃ (J \cap 𝒫 S) \in V$
16	5 8 12 15	fvmptd3	$⊢ (J \in Top \land S \subseteq X) \to (x \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 x)) (S) = ⋃ (J \cap 𝒫 S)$
17	4 16	eqtrd	$⊢ (J \in Top \land S \subseteq X) \to int (J) (S) = ⋃ (J \cap 𝒫 S)$