Theorem ntrclselnel1

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then there is an equivalence between membership in the interior of a set and non-membership in the closure of the complement of the set. (Contributed by RP, 28-May-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 )
	ntrcls.x	|- ( ph -> X e. B )
	ntrcls.s	|- ( ph -> S e. ~P B )
Assertion	ntrclselnel1	|- ( ph -> ( X e. ( I ` S ) <-> -. X e. ( 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		ntrcls.x	|- ( ph -> X e. B )
5		ntrcls.s	|- ( ph -> S e. ~P B )
6	1 2 3	ntrclsfv2	|- ( ph -> ( D ` K ) = I )
7	6	eqcomd	|- ( ph -> I = ( D ` K ) )
8	7	fveq1d	|- ( ph -> ( I ` S ) = ( ( D ` K ) ` S ) )
9	2 3	ntrclsbex	|- ( ph -> B e. _V )
10	1 2 3	ntrclskex	|- ( ph -> K e. ( ~P B ^m ~P B ) )
11		eqid	|- ( D ` K ) = ( D ` K )
12		eqid	|- ( ( D ` K ) ` S ) = ( ( D ` K ) ` S )
13	1 2 9 10 11 5 12	dssmapfv3d	|- ( ph -> ( ( D ` K ) ` S ) = ( B \ ( K ` ( B \ S ) ) ) )
14	8 13	eqtrd	|- ( ph -> ( I ` S ) = ( B \ ( K ` ( B \ S ) ) ) )
15	14	eleq2d	|- ( ph -> ( X e. ( I ` S ) <-> X e. ( B \ ( K ` ( B \ S ) ) ) ) )
16		eldif	|- ( X e. ( B \ ( K ` ( B \ S ) ) ) <-> ( X e. B /\ -. X e. ( K ` ( B \ S ) ) ) )
17	16	a1i	|- ( ph -> ( X e. ( B \ ( K ` ( B \ S ) ) ) <-> ( X e. B /\ -. X e. ( K ` ( B \ S ) ) ) ) )
18	4 17	mpbirand	|- ( ph -> ( X e. ( B \ ( K ` ( B \ S ) ) ) <-> -. X e. ( K ` ( B \ S ) ) ) )
19	15 18	bitrd	|- ( ph -> ( X e. ( I ` S ) <-> -. X e. ( K ` ( B \ S ) ) ) )