Metamath Proof Explorer

Theorem ntrneinex

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then the neighborhood function exists. (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	ntrneinex	$⊢ φ \to N \in ({𝒫 𝒫 B}^{B})$

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		f1orel	$⊢ F : {𝒫 B}^{𝒫 B} \underset{1-1 onto}{⟶} {𝒫 𝒫 B}^{B} \to Rel F$
6	4 5	syl	$⊢ φ \to Rel F$
7		relelrn	$⊢ (Rel F \land I F N) \to N \in ran F$
8	6 3 7	syl2anc	$⊢ φ \to N \in ran F$
9		dff1o2	$⊢ F : {𝒫 B}^{𝒫 B} \underset{1-1 onto}{⟶} {𝒫 𝒫 B}^{B} \leftrightarrow (F Fn ({𝒫 B}^{𝒫 B}) \land Fun F^{-1} \land ran F = {𝒫 𝒫 B}^{B})$
10	4 9	sylib	$⊢ φ \to (F Fn ({𝒫 B}^{𝒫 B}) \land Fun F^{-1} \land ran F = {𝒫 𝒫 B}^{B})$
11	10	simp3d	$⊢ φ \to ran F = {𝒫 𝒫 B}^{B}$
12	8 11	eleqtrd	$⊢ φ \to N \in ({𝒫 𝒫 B}^{B})$