Theorem ntrrn

Description: The range of the interior function of a topology a subset of the open sets of the topology. (Contributed by RP, 22-Apr-2021)

	Ref	Expression
Hypotheses	ntrrn.x	⊢ 𝑋 = ∪ 𝐽
	ntrrn.i	⊢ 𝐼 = ( int ‘ 𝐽 )
Assertion	ntrrn	⊢ ( 𝐽 ∈ Top → ran 𝐼 ⊆ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		ntrrn.x	⊢ 𝑋 = ∪ 𝐽
2		ntrrn.i	⊢ 𝐼 = ( int ‘ 𝐽 )
3	2	rneqi	⊢ ran 𝐼 = ran ( int ‘ 𝐽 )
4		vpwex	⊢ 𝒫 𝑠 ∈ V
5	4	inex2	⊢ ( 𝐽 ∩ 𝒫 𝑠 ) ∈ V
6	5	uniex	⊢ ∪ ( 𝐽 ∩ 𝒫 𝑠 ) ∈ V
7	6	rgenw	⊢ ∀ 𝑠 ∈ 𝒫 𝑋 ∪ ( 𝐽 ∩ 𝒫 𝑠 ) ∈ V
8		nfcv	⊢ Ⅎ 𝑠 𝒫 𝑋
9	8	fnmptf	⊢ ( ∀ 𝑠 ∈ 𝒫 𝑋 ∪ ( 𝐽 ∩ 𝒫 𝑠 ) ∈ V → ( 𝑠 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑠 ) ) Fn 𝒫 𝑋 )
10	7 9	mp1i	⊢ ( 𝐽 ∈ Top → ( 𝑠 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑠 ) ) Fn 𝒫 𝑋 )
11	1	ntrfval	⊢ ( 𝐽 ∈ Top → ( int ‘ 𝐽 ) = ( 𝑠 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑠 ) ) )
12	11	fneq1d	⊢ ( 𝐽 ∈ Top → ( ( int ‘ 𝐽 ) Fn 𝒫 𝑋 ↔ ( 𝑠 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑠 ) ) Fn 𝒫 𝑋 ) )
13	10 12	mpbird	⊢ ( 𝐽 ∈ Top → ( int ‘ 𝐽 ) Fn 𝒫 𝑋 )
14		elpwi	⊢ ( 𝑠 ∈ 𝒫 𝑋 → 𝑠 ⊆ 𝑋 )
15	1	ntropn	⊢ ( ( 𝐽 ∈ Top ∧ 𝑠 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑠 ) ∈ 𝐽 )
16	15	ex	⊢ ( 𝐽 ∈ Top → ( 𝑠 ⊆ 𝑋 → ( ( int ‘ 𝐽 ) ‘ 𝑠 ) ∈ 𝐽 ) )
17	14 16	syl5	⊢ ( 𝐽 ∈ Top → ( 𝑠 ∈ 𝒫 𝑋 → ( ( int ‘ 𝐽 ) ‘ 𝑠 ) ∈ 𝐽 ) )
18	17	ralrimiv	⊢ ( 𝐽 ∈ Top → ∀ 𝑠 ∈ 𝒫 𝑋 ( ( int ‘ 𝐽 ) ‘ 𝑠 ) ∈ 𝐽 )
19		fnfvrnss	⊢ ( ( ( int ‘ 𝐽 ) Fn 𝒫 𝑋 ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ( ( int ‘ 𝐽 ) ‘ 𝑠 ) ∈ 𝐽 ) → ran ( int ‘ 𝐽 ) ⊆ 𝐽 )
20	13 18 19	syl2anc	⊢ ( 𝐽 ∈ Top → ran ( int ‘ 𝐽 ) ⊆ 𝐽 )
21	3 20	eqsstrid	⊢ ( 𝐽 ∈ Top → ran 𝐼 ⊆ 𝐽 )