Theorem ntrclsneine0

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then conditions equal to claiming that for every point, at least one (pseudo-)neighborbood exists hold equally. (Contributed by RP, 21-May-2021)

	Ref	Expression
Hypotheses	ntrcls.o	$$⊢O=\left(i\in \mathrm{V}⟼\left(k\in \left({𝒫i}^{𝒫i}\right)⟼\left(j\in 𝒫i⟼i\setminus k\left(i\setminus j\right)\right)\right)\right)$$
	ntrcls.d	$$⊢D=O\left(B\right)$$
	ntrcls.r	$$⊢\phi \to IDK$$
Assertion	ntrclsneine0	$$⊢\phi \to \left(\forall x\in B\exists s\in 𝒫Bx\in I\left(s\right)\leftrightarrow \forall x\in B\exists s\in 𝒫B\neg x\in K\left(s\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ntrcls.o	$$⊢O=\left(i\in \mathrm{V}⟼\left(k\in \left({𝒫i}^{𝒫i}\right)⟼\left(j\in 𝒫i⟼i\setminus k\left(i\setminus j\right)\right)\right)\right)$$
2		ntrcls.d	$$⊢D=O\left(B\right)$$
3		ntrcls.r	$$⊢\phi \to IDK$$
4	3	adantr	$$⊢\left(\phi \wedge x\in B\right)\to IDK$$
5		simpr	$$⊢\left(\phi \wedge x\in B\right)\to x\in B$$
6	1 2 4 5	ntrclsneine0lem	$$⊢\left(\phi \wedge x\in B\right)\to \left(\exists s\in 𝒫Bx\in I\left(s\right)\leftrightarrow \exists s\in 𝒫B\neg x\in K\left(s\right)\right)$$
7	6	ralbidva	$$⊢\phi \to \left(\forall x\in B\exists s\in 𝒫Bx\in I\left(s\right)\leftrightarrow \forall x\in B\exists s\in 𝒫B\neg x\in K\left(s\right)\right)$$