Metamath Proof Explorer

Theorem ntrneineine1lem

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then conditions equal to claiming that for every point, at not all subsets are (pseudo-)neighborboods hold equally. (Contributed by RP, 1-Jun-2021)

Ref Expression
Hypotheses ntrnei.o ⊢O=i∈V,j∈V⟼k∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m
ntrnei.f ⊢F=𝒫BOB
ntrnei.r ⊢φ→IFN
ntrnei.x ⊢φ→X∈B
Assertion ntrneineine1lem ⊢φ→∃s∈𝒫B¬X∈I⁡s↔N⁡X≠𝒫B

Proof

Step Hyp Ref Expression
1 ntrnei.o ⊢O=i∈V,j∈V⟼k∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m
2 ntrnei.f ⊢F=𝒫BOB
3 ntrnei.r ⊢φ→IFN
4 ntrnei.x ⊢φ→X∈B
5 3 adantr ⊢φ∧s∈𝒫B→IFN
6 4 adantr ⊢φ∧s∈𝒫B→X∈B
7 simpr ⊢φ∧s∈𝒫B→s∈𝒫B
8 1 2 5 6 7 ntrneiel ⊢φ∧s∈𝒫B→X∈I⁡s↔s∈N⁡X
9 8 notbid ⊢φ∧s∈𝒫B→¬X∈I⁡s↔¬s∈N⁡X
10 9 rexbidva ⊢φ→∃s∈𝒫B¬X∈I⁡s↔∃s∈𝒫B¬s∈N⁡X
11 1 2 3 ntrneinex ⊢φ→N∈𝒫𝒫BB
12 elmapi ⊢N∈𝒫𝒫BB→N:B⟶𝒫𝒫B
13 11 12 syl ⊢φ→N:B⟶𝒫𝒫B
14 13 4 ffvelcdmd ⊢φ→N⁡X∈𝒫𝒫B
15 14 elpwid ⊢φ→N⁡X⊆𝒫B
16 biortn ⊢N⁡X⊆𝒫B→¬𝒫B⊆N⁡X↔¬N⁡X⊆𝒫B∨¬𝒫B⊆N⁡X
17 15 16 syl ⊢φ→¬𝒫B⊆N⁡X↔¬N⁡X⊆𝒫B∨¬𝒫B⊆N⁡X
18 df-rex ⊢∃s∈𝒫B¬s∈N⁡X↔∃ss∈𝒫B∧¬s∈N⁡X
19 nss ⊢¬𝒫B⊆N⁡X↔∃ss∈𝒫B∧¬s∈N⁡X
20 18 19 bitr4i ⊢∃s∈𝒫B¬s∈N⁡X↔¬𝒫B⊆N⁡X
21 df-ne ⊢N⁡X≠𝒫B↔¬N⁡X=𝒫B
22 ianor ⊢¬N⁡X⊆𝒫B∧𝒫B⊆N⁡X↔¬N⁡X⊆𝒫B∨¬𝒫B⊆N⁡X
23 eqss ⊢N⁡X=𝒫B↔N⁡X⊆𝒫B∧𝒫B⊆N⁡X
24 22 23 xchnxbir ⊢¬N⁡X=𝒫B↔¬N⁡X⊆𝒫B∨¬𝒫B⊆N⁡X
25 21 24 bitri ⊢N⁡X≠𝒫B↔¬N⁡X⊆𝒫B∨¬𝒫B⊆N⁡X
26 17 20 25 3bitr4g ⊢φ→∃s∈𝒫B¬s∈N⁡X↔N⁡X≠𝒫B
27 10 26 bitrd ⊢φ→∃s∈𝒫B¬X∈I⁡s↔N⁡X≠𝒫B