Theorem ntrclsfveq

Description: If interior and closure functions are related then equality of a pair of function values is equivalent to equality of a pair of the other function's values. (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.t	|- ( ph -> T e. ~P B )
Assertion	ntrclsfveq	|- ( ph -> ( ( I ` S ) = ( I ` T ) <-> ( K ` ( B \ S ) ) = ( K ` ( B \ T ) ) ) )

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.t	|- ( ph -> T e. ~P B )
6	1 2 3 5	ntrclsfv	|- ( ph -> ( I ` T ) = ( B \ ( K ` ( B \ T ) ) ) )
7	6	eqeq2d	|- ( ph -> ( ( I ` S ) = ( I ` T ) <-> ( I ` S ) = ( B \ ( K ` ( B \ T ) ) ) ) )
8	2 3	ntrclsrcomplex	|- ( ph -> ( B \ ( K ` ( B \ T ) ) ) e. ~P B )
9	1 2 3 4 8	ntrclsfveq1	|- ( ph -> ( ( I ` S ) = ( B \ ( K ` ( B \ T ) ) ) <-> ( K ` ( B \ S ) ) = ( B \ ( B \ ( K ` ( B \ T ) ) ) ) ) )
10	1 2 3	ntrclskex	|- ( ph -> K e. ( ~P B ^m ~P B ) )
11		elmapi	|- ( K e. ( ~P B ^m ~P B ) -> K : ~P B --> ~P B )
12	10 11	syl	|- ( ph -> K : ~P B --> ~P B )
13	2 3	ntrclsrcomplex	|- ( ph -> ( B \ T ) e. ~P B )
14	12 13	ffvelcdmd	|- ( ph -> ( K ` ( B \ T ) ) e. ~P B )
15	14	elpwid	|- ( ph -> ( K ` ( B \ T ) ) C_ B )
16		dfss4	|- ( ( K ` ( B \ T ) ) C_ B <-> ( B \ ( B \ ( K ` ( B \ T ) ) ) ) = ( K ` ( B \ T ) ) )
17	15 16	sylib	|- ( ph -> ( B \ ( B \ ( K ` ( B \ T ) ) ) ) = ( K ` ( B \ T ) ) )
18	17	eqeq2d	|- ( ph -> ( ( K ` ( B \ S ) ) = ( B \ ( B \ ( K ` ( B \ T ) ) ) ) <-> ( K ` ( B \ S ) ) = ( K ` ( B \ T ) ) ) )
19	7 9 18	3bitrd	|- ( ph -> ( ( I ` S ) = ( I ` T ) <-> ( K ` ( B \ S ) ) = ( K ` ( B \ T ) ) ) )