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=\bigcup J$$
Assertion	ntrfval	$$⊢J\in \mathrm{Top}\to \mathrm{int}\left(J\right)=\left(x\in 𝒫X⟼\bigcup \left(J\cap 𝒫x\right)\right)$$

Proof

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