Metamath Proof Explorer

Theorem ntrneifv1

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then the function value of F is the neighborhood function. (Contributed by RP, 29-May-2021)

		Ref	Expression
	Hypotheses	ntrnei.o	$⊢ O = (i \in V, j \in V ⟼ (k \in ({𝒫 j}^{i}) ⟼ (l \in j ⟼ \{m \in i \| l \in k (m)\})))$
		ntrnei.f	$⊢ F = 𝒫 B O B$
		ntrnei.r	$⊢ φ \to I F N$
	Assertion	ntrneifv1	$⊢ φ \to F (I) = N$

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	$⊢ O = (i \in V, j \in V ⟼ (k \in ({𝒫 j}^{i}) ⟼ (l \in j ⟼ \{m \in i \| l \in k (m)\})))$
2		ntrnei.f	$⊢ F = 𝒫 B O B$
3		ntrnei.r	$⊢ φ \to I F N$
4	1 2 3	ntrneif1o	$⊢ φ \to F : {𝒫 B}^{𝒫 B} \underset{1-1 onto}{⟶} {𝒫 𝒫 B}^{B}$
5		f1ofn	$⊢ F : {𝒫 B}^{𝒫 B} \underset{1-1 onto}{⟶} {𝒫 𝒫 B}^{B} \to F Fn ({𝒫 B}^{𝒫 B})$
6	4 5	syl	$⊢ φ \to F Fn ({𝒫 B}^{𝒫 B})$
7	1 2 3	ntrneiiex	$⊢ φ \to I \in ({𝒫 B}^{𝒫 B})$
8	6 7	jca	$⊢ φ \to (F Fn ({𝒫 B}^{𝒫 B}) \land I \in ({𝒫 B}^{𝒫 B}))$
9		fnfun	$⊢ F Fn ({𝒫 B}^{𝒫 B}) \to Fun F$
10	9	adantr	$⊢ (F Fn ({𝒫 B}^{𝒫 B}) \land I \in ({𝒫 B}^{𝒫 B})) \to Fun F$
11		fndm	$⊢ F Fn ({𝒫 B}^{𝒫 B}) \to dom F = {𝒫 B}^{𝒫 B}$
12	11	eleq2d	$⊢ F Fn ({𝒫 B}^{𝒫 B}) \to (I \in dom F \leftrightarrow I \in ({𝒫 B}^{𝒫 B}))$
13	12	biimpar	$⊢ (F Fn ({𝒫 B}^{𝒫 B}) \land I \in ({𝒫 B}^{𝒫 B})) \to I \in dom F$
14	10 13	jca	$⊢ (F Fn ({𝒫 B}^{𝒫 B}) \land I \in ({𝒫 B}^{𝒫 B})) \to (Fun F \land I \in dom F)$
15		funbrfvb	$⊢ (Fun F \land I \in dom F) \to (F (I) = N \leftrightarrow I F N)$
16	8 14 15	3syl	$⊢ φ \to (F (I) = N \leftrightarrow I F N)$
17	3 16	mpbird	$⊢ φ \to F (I) = N$