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

Metamath Proof Explorer

Theorem ntrfval

Description: The interior function on the subsets of a topology's base set. (Contributed by NM, 10-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013)

		Ref	Expression
	Hypothesis	cldval.1	$⊢ X = ⋃ J$
	Assertion	ntrfval	$⊢ J \in Top \to int (J) = (x \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 x))$

Proof

Step	Hyp	Ref	Expression
1		cldval.1	$⊢ X = ⋃ J$
2	1	topopn	$⊢ J \in Top \to X \in J$
3		pwexg	$⊢ X \in J \to 𝒫 X \in V$
4		mptexg	$⊢ 𝒫 X \in V \to (x \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 x)) \in V$
5	2 3 4	3syl	$⊢ J \in Top \to (x \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 x)) \in V$
6		unieq	$⊢ j = J \to ⋃ j = ⋃ J$
7	6 1	eqtr4di	$⊢ j = J \to ⋃ j = X$
8	7	pweqd	$⊢ j = J \to 𝒫 ⋃ j = 𝒫 X$
9		ineq1	$⊢ j = J \to j \cap 𝒫 x = J \cap 𝒫 x$
10	9	unieqd	$⊢ j = J \to ⋃ (j \cap 𝒫 x) = ⋃ (J \cap 𝒫 x)$
11	8 10	mpteq12dv	$⊢ j = J \to (x \in 𝒫 ⋃ j ⟼ ⋃ (j \cap 𝒫 x)) = (x \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 x))$
12		df-ntr	$⊢ int = (j \in Top ⟼ (x \in 𝒫 ⋃ j ⟼ ⋃ (j \cap 𝒫 x)))$
13	11 12	fvmptg	$⊢ (J \in Top \land (x \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 x)) \in V) \to int (J) = (x \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 x))$
14	5 13	mpdan	$⊢ J \in Top \to int (J) = (x \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 x))$