Theorem ntrclsfveq2

Description: If interior and closure functions are related then specific function values are complementary. (Contributed by RP, 27-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 )
	ntrclsfv.c	|- ( ph -> C e. ~P B )
Assertion	ntrclsfveq2	|- ( ph -> ( ( I ` ( B \ S ) ) = C <-> ( K ` S ) = ( B \ C ) ) )

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		ntrclsfv.c	|- ( ph -> C e. ~P B )
6	1 2 3	ntrclsiex	|- ( ph -> I e. ( ~P B ^m ~P B ) )
7		elmapi	|- ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
8	6 7	syl	|- ( ph -> I : ~P B --> ~P B )
9	2 3	ntrclsrcomplex	|- ( ph -> ( B \ S ) e. ~P B )
10	8 9	ffvelrnd	|- ( ph -> ( I ` ( B \ S ) ) e. ~P B )
11	10	elpwid	|- ( ph -> ( I ` ( B \ S ) ) C_ B )
12	5	elpwid	|- ( ph -> C C_ B )
13		rcompleq	|- ( ( ( I ` ( B \ S ) ) C_ B /\ C C_ B ) -> ( ( I ` ( B \ S ) ) = C <-> ( B \ ( I ` ( B \ S ) ) ) = ( B \ C ) ) )
14	11 12 13	syl2anc	|- ( ph -> ( ( I ` ( B \ S ) ) = C <-> ( B \ ( I ` ( B \ S ) ) ) = ( B \ C ) ) )
15	1 2 3	ntrclsnvobr	|- ( ph -> K D I )
16	1 2 15 4	ntrclsfv	|- ( ph -> ( K ` S ) = ( B \ ( I ` ( B \ S ) ) ) )
17	16	eqeq1d	|- ( ph -> ( ( K ` S ) = ( B \ C ) <-> ( B \ ( I ` ( B \ S ) ) ) = ( B \ C ) ) )
18	14 17	bitr4d	|- ( ph -> ( ( I ` ( B \ S ) ) = C <-> ( K ` S ) = ( B \ C ) ) )