Theorem ntrclsiex

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	ntrclsiex	|- ( ph -> I 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	ntrclsf1o	|- ( ph -> D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) )
5		f1orel	|- ( D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) -> Rel D )
6	4 5	syl	|- ( ph -> Rel D )
7		releldm	|- ( ( Rel D /\ I D K ) -> I e. dom D )
8	6 3 7	syl2anc	|- ( ph -> I e. dom D )
9		f1odm	|- ( D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) -> dom D = ( ~P B ^m ~P B ) )
10	4 9	syl	|- ( ph -> dom D = ( ~P B ^m ~P B ) )
11	8 10	eleqtrd	|- ( ph -> I e. ( ~P B ^m ~P B ) )