Theorem ntrf

Description: The interior function of a topology is a map from the powerset of the base set to the open sets of the topology. (Contributed by RP, 22-Apr-2021)

	Ref	Expression
Hypotheses	ntrrn.x	⊢ 𝑋 = ∪ 𝐽
	ntrrn.i	⊢ 𝐼 = ( int ‘ 𝐽 )
Assertion	ntrf	⊢ ( 𝐽 ∈ Top → 𝐼 : 𝒫 𝑋 ⟶ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		ntrrn.x	⊢ 𝑋 = ∪ 𝐽
2		ntrrn.i	⊢ 𝐼 = ( int ‘ 𝐽 )
3		vpwex	⊢ 𝒫 𝑠 ∈ V
4	3	inex2	⊢ ( 𝐽 ∩ 𝒫 𝑠 ) ∈ V
5	4	uniex	⊢ ∪ ( 𝐽 ∩ 𝒫 𝑠 ) ∈ V
6		eqid	⊢ ( 𝑠 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑠 ) ) = ( 𝑠 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑠 ) )
7	5 6	fnmpti	⊢ ( 𝑠 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑠 ) ) Fn 𝒫 𝑋
8	1	ntrfval	⊢ ( 𝐽 ∈ Top → ( int ‘ 𝐽 ) = ( 𝑠 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑠 ) ) )
9	2 8	eqtrid	⊢ ( 𝐽 ∈ Top → 𝐼 = ( 𝑠 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑠 ) ) )
10	9	fneq1d	⊢ ( 𝐽 ∈ Top → ( 𝐼 Fn 𝒫 𝑋 ↔ ( 𝑠 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑠 ) ) Fn 𝒫 𝑋 ) )
11	7 10	mpbiri	⊢ ( 𝐽 ∈ Top → 𝐼 Fn 𝒫 𝑋 )
12	1 2	ntrrn	⊢ ( 𝐽 ∈ Top → ran 𝐼 ⊆ 𝐽 )
13		df-f	⊢ ( 𝐼 : 𝒫 𝑋 ⟶ 𝐽 ↔ ( 𝐼 Fn 𝒫 𝑋 ∧ ran 𝐼 ⊆ 𝐽 ) )
14	11 12 13	sylanbrc	⊢ ( 𝐽 ∈ Top → 𝐼 : 𝒫 𝑋 ⟶ 𝐽 )