Theorem ntrclskex

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then those functions are maps of subsets to subsets. (Contributed by RP, 21-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 )
Assertion	ntrclskex	|- ( ph -> K e. ( ~P B ^m ~P B ) )

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	1 2 3	ntrclsnvobr	|- ( ph -> K D I )
5	1 2 4	ntrclsiex	|- ( ph -> K e. ( ~P B ^m ~P B ) )