Theorem ntrclsfv1

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then there is a functional relation between them (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 )
Assertion	ntrclsfv1	|- ( ph -> ( D ` I ) = K )

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		f1ofn	|- ( D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) -> D Fn ( ~P B ^m ~P B ) )
6	4 5	syl	|- ( ph -> D Fn ( ~P B ^m ~P B ) )
7	1 2 3	ntrclsiex	|- ( ph -> I e. ( ~P B ^m ~P B ) )
8	6 7	jca	|- ( ph -> ( D Fn ( ~P B ^m ~P B ) /\ I e. ( ~P B ^m ~P B ) ) )
9		fnfun	|- ( D Fn ( ~P B ^m ~P B ) -> Fun D )
10	9	adantr	|- ( ( D Fn ( ~P B ^m ~P B ) /\ I e. ( ~P B ^m ~P B ) ) -> Fun D )
11		fndm	|- ( D Fn ( ~P B ^m ~P B ) -> dom D = ( ~P B ^m ~P B ) )
12	11	eleq2d	|- ( D Fn ( ~P B ^m ~P B ) -> ( I e. dom D <-> I e. ( ~P B ^m ~P B ) ) )
13	12	biimpar	|- ( ( D Fn ( ~P B ^m ~P B ) /\ I e. ( ~P B ^m ~P B ) ) -> I e. dom D )
14	10 13	jca	|- ( ( D Fn ( ~P B ^m ~P B ) /\ I e. ( ~P B ^m ~P B ) ) -> ( Fun D /\ I e. dom D ) )
15	8 14	syl	|- ( ph -> ( Fun D /\ I e. dom D ) )
16		funbrfvb	|- ( ( Fun D /\ I e. dom D ) -> ( ( D ` I ) = K <-> I D K ) )
17	15 16	syl	|- ( ph -> ( ( D ` I ) = K <-> I D K ) )
18	3 17	mpbird	|- ( ph -> ( D ` I ) = K )