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 = U. J
	ntrrn.i	|- I = ( int ` J )
Assertion	ntrrn	|- ( J e. Top -> ran I C_ J )

Proof

Step	Hyp	Ref	Expression
1		ntrrn.x	|- X = U. J
2		ntrrn.i	|- I = ( int ` J )
3	2	rneqi	|- ran I = ran ( int ` J )
4		vpwex	|- ~P s e. _V
5	4	inex2	|- ( J i^i ~P s ) e. _V
6	5	uniex	|- U. ( J i^i ~P s ) e. _V
7	6	rgenw	|- A. s e. ~P X U. ( J i^i ~P s ) e. _V
8		nfcv	|- F/_ s ~P X
9	8	fnmptf	|- ( A. s e. ~P X U. ( J i^i ~P s ) e. _V -> ( s e. ~P X |-> U. ( J i^i ~P s ) ) Fn ~P X )
10	7 9	mp1i	|- ( J e. Top -> ( s e. ~P X |-> U. ( J i^i ~P s ) ) Fn ~P X )
11	1	ntrfval	|- ( J e. Top -> ( int ` J ) = ( s e. ~P X |-> U. ( J i^i ~P s ) ) )
12	11	fneq1d	|- ( J e. Top -> ( ( int ` J ) Fn ~P X <-> ( s e. ~P X |-> U. ( J i^i ~P s ) ) Fn ~P X ) )
13	10 12	mpbird	|- ( J e. Top -> ( int ` J ) Fn ~P X )
14		elpwi	|- ( s e. ~P X -> s C_ X )
15	1	ntropn	|- ( ( J e. Top /\ s C_ X ) -> ( ( int ` J ) ` s ) e. J )
16	15	ex	|- ( J e. Top -> ( s C_ X -> ( ( int ` J ) ` s ) e. J ) )
17	14 16	syl5	|- ( J e. Top -> ( s e. ~P X -> ( ( int ` J ) ` s ) e. J ) )
18	17	ralrimiv	|- ( J e. Top -> A. s e. ~P X ( ( int ` J ) ` s ) e. J )
19		fnfvrnss	|- ( ( ( int ` J ) Fn ~P X /\ A. s e. ~P X ( ( int ` J ) ` s ) e. J ) -> ran ( int ` J ) C_ J )
20	13 18 19	syl2anc	|- ( J e. Top -> ran ( int ` J ) C_ J )
21	3 20	eqsstrid	|- ( J e. Top -> ran I C_ J )