Theorem ntrclsfv

Description: The value of the interior (closure) expressed in terms of the closure (interior). (Contributed by RP, 25-Jun-2021)

	Ref	Expression
Hypotheses	ntrcls.o	|- O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) )
	ntrcls.d	|- D = ( O ` B )
	ntrcls.r	|- ( ph -> I D K )
	ntrclsfv.s	|- ( ph -> S e. ~P B )
Assertion	ntrclsfv	|- ( ph -> ( I ` S ) = ( B \ ( K ` ( B \ S ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ntrcls.o	|- O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) )
2		ntrcls.d	|- D = ( O ` B )
3		ntrcls.r	|- ( ph -> I D K )
4		ntrclsfv.s	|- ( ph -> S e. ~P B )
5	1 2 3	ntrclsfv2	|- ( ph -> ( D ` K ) = I )
6	5	fveq1d	|- ( ph -> ( ( D ` K ) ` S ) = ( I ` S ) )
7	2 3	ntrclsbex	|- ( ph -> B e. _V )
8	1 2 3	ntrclskex	|- ( ph -> K e. ( ~P B ^m ~P B ) )
9		eqid	|- ( D ` K ) = ( D ` K )
10		eqid	|- ( ( D ` K ) ` S ) = ( ( D ` K ) ` S )
11	1 2 7 8 9 4 10	dssmapfv3d	|- ( ph -> ( ( D ` K ) ` S ) = ( B \ ( K ` ( B \ S ) ) ) )
12	6 11	eqtr3d	|- ( ph -> ( I ` S ) = ( B \ ( K ` ( B \ S ) ) ) )