ntrneiel

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then there is an equivalence between membership in the interior of a set and non-membership in the closure of the complement of the set. (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$
	ntrnei.x	$⊢ φ \to X \in B$
	ntrnei.s	$⊢ φ \to S \in 𝒫 B$
Assertion	ntrneiel	$⊢ φ \to (X \in I (S) \leftrightarrow S \in N (X))$

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		ntrnei.x	$⊢ φ \to X \in B$
5		ntrnei.s	$⊢ φ \to S \in 𝒫 B$
6		fveq2	$⊢ m = S \to I (m) = I (S)$
7	6	eleq2d	$⊢ m = S \to (X \in I (m) \leftrightarrow X \in I (S))$
8	7	elrab3	$⊢ S \in 𝒫 B \to (S \in \{m \in 𝒫 B \| X \in I (m)\} \leftrightarrow X \in I (S))$
9	5 8	syl	$⊢ φ \to (S \in \{m \in 𝒫 B \| X \in I (m)\} \leftrightarrow X \in I (S))$
10	1 2 3	ntrneibex	$⊢ φ \to B \in V$
11	10	pwexd	$⊢ φ \to 𝒫 B \in V$
12	1 2 3	ntrneiiex	$⊢ φ \to I \in ({𝒫 B}^{𝒫 B})$
13		eqid	$⊢ F (I) = F (I)$
14	1 11 10 2 12 13 4	fsovfvfvd	$⊢ φ \to F (I) (X) = \{m \in 𝒫 B \| X \in I (m)\}$
15	1 2 3	ntrneifv1	$⊢ φ \to F (I) = N$
16	15	fveq1d	$⊢ φ \to F (I) (X) = N (X)$
17	14 16	eqtr3d	$⊢ φ \to \{m \in 𝒫 B \| X \in I (m)\} = N (X)$
18	17	eleq2d	$⊢ φ \to (S \in \{m \in 𝒫 B \| X \in I (m)\} \leftrightarrow S \in N (X))$
19	9 18	bitr3d	$⊢ φ \to (X \in I (S) \leftrightarrow S \in N (X))$

Metamath Proof Explorer

Theorem ntrneiel

Proof