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)

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 \in V$
5	4	inex2	$⊢ J \cap 𝒫 s \in V$
6	5	uniex	$⊢ ⋃ (J \cap 𝒫 s) \in V$
7	6	rgenw	$⊢ \forall s \in 𝒫 X ⋃ (J \cap 𝒫 s) \in V$
8		nfcv	$⊢ \underline{Ⅎ} s 𝒫 X$
9	8	fnmptf	$⊢ \forall s \in 𝒫 X ⋃ (J \cap 𝒫 s) \in V \to (s \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 s)) Fn 𝒫 X$
10	7 9	mp1i	$⊢ J \in Top \to (s \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 s)) Fn 𝒫 X$
11	1	ntrfval	$⊢ J \in Top \to int (J) = (s \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 s))$
12	11	fneq1d	$⊢ J \in Top \to (int (J) Fn 𝒫 X \leftrightarrow (s \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 s)) Fn 𝒫 X)$
13	10 12	mpbird	$⊢ J \in Top \to int (J) Fn 𝒫 X$
14		elpwi	$⊢ s \in 𝒫 X \to s \subseteq X$
15	1	ntropn	$⊢ (J \in Top \land s \subseteq X) \to int (J) (s) \in J$
16	15	ex	$⊢ J \in Top \to (s \subseteq X \to int (J) (s) \in J)$
17	14 16	syl5	$⊢ J \in Top \to (s \in 𝒫 X \to int (J) (s) \in J)$
18	17	ralrimiv	$⊢ J \in Top \to \forall s \in 𝒫 X int (J) (s) \in J$
19		fnfvrnss	$⊢ (int (J) Fn 𝒫 X \land \forall s \in 𝒫 X int (J) (s) \in J) \to ran int (J) \subseteq J$
20	13 18 19	syl2anc	$⊢ J \in Top \to ran int (J) \subseteq J$
21	3 20	eqsstrid	$⊢ J \in Top \to ran I \subseteq J$

Metamath Proof Explorer