Metamath Proof Explorer

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 \in V ⟼ (k \in ({𝒫 i}^{𝒫 i}) ⟼ (j \in 𝒫 i ⟼ i ∖ k (i ∖ j))))$
		ntrcls.d	$⊢ D = O (B)$
		ntrcls.r	$⊢ φ \to I D K$
	Assertion	ntrclsfv1	$⊢ φ \to D (I) = K$

Proof

Step	Hyp	Ref	Expression
1		ntrcls.o	$⊢ O = (i \in V ⟼ (k \in ({𝒫 i}^{𝒫 i}) ⟼ (j \in 𝒫 i ⟼ i ∖ k (i ∖ j))))$
2		ntrcls.d	$⊢ D = O (B)$
3		ntrcls.r	$⊢ φ \to I D K$
4	1 2 3	ntrclsf1o	$⊢ φ \to D : {𝒫 B}^{𝒫 B} \underset{1-1 onto}{⟶} {𝒫 B}^{𝒫 B}$
5		f1ofn	$⊢ D : {𝒫 B}^{𝒫 B} \underset{1-1 onto}{⟶} {𝒫 B}^{𝒫 B} \to D Fn ({𝒫 B}^{𝒫 B})$
6	4 5	syl	$⊢ φ \to D Fn ({𝒫 B}^{𝒫 B})$
7	1 2 3	ntrclsiex	$⊢ φ \to I \in ({𝒫 B}^{𝒫 B})$
8	6 7	jca	$⊢ φ \to (D Fn ({𝒫 B}^{𝒫 B}) \land I \in ({𝒫 B}^{𝒫 B}))$
9		fnfun	$⊢ D Fn ({𝒫 B}^{𝒫 B}) \to Fun D$
10	9	adantr	$⊢ (D Fn ({𝒫 B}^{𝒫 B}) \land I \in ({𝒫 B}^{𝒫 B})) \to Fun D$
11		fndm	$⊢ D Fn ({𝒫 B}^{𝒫 B}) \to dom D = {𝒫 B}^{𝒫 B}$
12	11	eleq2d	$⊢ D Fn ({𝒫 B}^{𝒫 B}) \to (I \in dom D \leftrightarrow I \in ({𝒫 B}^{𝒫 B}))$
13	12	biimpar	$⊢ (D Fn ({𝒫 B}^{𝒫 B}) \land I \in ({𝒫 B}^{𝒫 B})) \to I \in dom D$
14	10 13	jca	$⊢ (D Fn ({𝒫 B}^{𝒫 B}) \land I \in ({𝒫 B}^{𝒫 B})) \to (Fun D \land I \in dom D)$
15	8 14	syl	$⊢ φ \to (Fun D \land I \in dom D)$
16		funbrfvb	$⊢ (Fun D \land I \in dom D) \to (D (I) = K \leftrightarrow I D K)$
17	15 16	syl	$⊢ φ \to (D (I) = K \leftrightarrow I D K)$
18	3 17	mpbird	$⊢ φ \to D (I) = K$