Metamath Proof Explorer

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 ⊢ X = ⋃ J
ntrrn.i ⊢ I = int ⁡ J
Assertion ntrrn ⊢ J ∈ Top → ran ⁡ I ⊆ J

Proof

Step Hyp Ref Expression
1 ntrrn.x ⊢ X = ⋃ J
2 ntrrn.i ⊢ I = int ⁡ J
3 2 rneqi ⊢ ran ⁡ I = ran ⁡ int ⁡ J
4 vpwex ⊢ 𝒫 s ∈ V
5 4 inex2 ⊢ J ∩ 𝒫 s ∈ V
6 5 uniex ⊢ ⋃ J ∩ 𝒫 s ∈ V
7 6 rgenw ⊢ ∀ s ∈ 𝒫 X ⋃ J ∩ 𝒫 s ∈ V
8 nfcv ⊢ Ⅎ _ s 𝒫 X
9 8 fnmptf ⊢ ∀ s ∈ 𝒫 X ⋃ J ∩ 𝒫 s ∈ V → s ∈ 𝒫 X ⟼ ⋃ J ∩ 𝒫 s Fn 𝒫 X
10 7 9 mp1i ⊢ J ∈ Top → s ∈ 𝒫 X ⟼ ⋃ J ∩ 𝒫 s Fn 𝒫 X
11 1 ntrfval ⊢ J ∈ Top → int ⁡ J = s ∈ 𝒫 X ⟼ ⋃ J ∩ 𝒫 s
12 11 fneq1d ⊢ J ∈ Top → int ⁡ J Fn 𝒫 X ↔ s ∈ 𝒫 X ⟼ ⋃ J ∩ 𝒫 s Fn 𝒫 X
13 10 12 mpbird ⊢ J ∈ Top → int ⁡ J Fn 𝒫 X
14 elpwi ⊢ s ∈ 𝒫 X → s ⊆ X
15 1 ntropn ⊢ J ∈ Top ∧ s ⊆ X → int ⁡ J ⁡ s ∈ J
16 15 ex ⊢ J ∈ Top → s ⊆ X → int ⁡ J ⁡ s ∈ J
17 14 16 syl5 ⊢ J ∈ Top → s ∈ 𝒫 X → int ⁡ J ⁡ s ∈ J
18 17 ralrimiv ⊢ J ∈ Top → ∀ s ∈ 𝒫 X int ⁡ J ⁡ s ∈ J
19 fnfvrnss ⊢ int ⁡ J Fn 𝒫 X ∧ ∀ s ∈ 𝒫 X int ⁡ J ⁡ s ∈ J → ran ⁡ int ⁡ J ⊆ J
20 13 18 19 syl2anc ⊢ J ∈ Top → ran ⁡ int ⁡ J ⊆ J
21 3 20 eqsstrid ⊢ J ∈ Top → ran ⁡ I ⊆ J