Metamath Proof Explorer

Theorem ntrclsneine0lem

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

Ref Expression
Hypotheses ntrcls.o ⊢ O = i ∈ V ⟼ k ∈ 𝒫 i 𝒫 i ⟼ j ∈ 𝒫 i ⟼ i ∖ k ⁡ i ∖ j
ntrcls.d ⊢ D = O ⁡ B
ntrcls.r ⊢ φ → I D K
ntrclslem0.x ⊢ φ → X ∈ B
Assertion ntrclsneine0lem ⊢ φ → ∃ s ∈ 𝒫 B X ∈ I ⁡ s ↔ ∃ s ∈ 𝒫 B ¬ X ∈ K ⁡ s

Proof

Step Hyp Ref Expression
1 ntrcls.o ⊢ O = i ∈ V ⟼ k ∈ 𝒫 i 𝒫 i ⟼ j ∈ 𝒫 i ⟼ i ∖ k ⁡ i ∖ j
2 ntrcls.d ⊢ D = O ⁡ B
3 ntrcls.r ⊢ φ → I D K
4 ntrclslem0.x ⊢ φ → X ∈ B
5 fveq2 ⊢ s = t → I ⁡ s = I ⁡ t
6 5 eleq2d ⊢ s = t → X ∈ I ⁡ s ↔ X ∈ I ⁡ t
7 6 cbvrexvw ⊢ ∃ s ∈ 𝒫 B X ∈ I ⁡ s ↔ ∃ t ∈ 𝒫 B X ∈ I ⁡ t
8 2 3 ntrclsrcomplex ⊢ φ → B ∖ s ∈ 𝒫 B
9 8 adantr ⊢ φ ∧ s ∈ 𝒫 B → B ∖ s ∈ 𝒫 B
10 2 3 ntrclsrcomplex ⊢ φ → B ∖ t ∈ 𝒫 B
11 10 adantr ⊢ φ ∧ t ∈ 𝒫 B → B ∖ t ∈ 𝒫 B
12 difeq2 ⊢ s = B ∖ t → B ∖ s = B ∖ B ∖ t
13 12 adantl ⊢ φ ∧ t ∈ 𝒫 B ∧ s = B ∖ t → B ∖ s = B ∖ B ∖ t
14 elpwi ⊢ t ∈ 𝒫 B → t ⊆ B
15 dfss4 ⊢ t ⊆ B ↔ B ∖ B ∖ t = t
16 14 15 sylib ⊢ t ∈ 𝒫 B → B ∖ B ∖ t = t
17 16 ad2antlr ⊢ φ ∧ t ∈ 𝒫 B ∧ s = B ∖ t → B ∖ B ∖ t = t
18 13 17 eqtr2d ⊢ φ ∧ t ∈ 𝒫 B ∧ s = B ∖ t → t = B ∖ s
19 11 18 rspcedeq2vd ⊢ φ ∧ t ∈ 𝒫 B → ∃ s ∈ 𝒫 B t = B ∖ s
20 fveq2 ⊢ t = B ∖ s → I ⁡ t = I ⁡ B ∖ s
21 20 eleq2d ⊢ t = B ∖ s → X ∈ I ⁡ t ↔ X ∈ I ⁡ B ∖ s
22 21 3ad2ant3 ⊢ φ ∧ s ∈ 𝒫 B ∧ t = B ∖ s → X ∈ I ⁡ t ↔ X ∈ I ⁡ B ∖ s
23 3 adantr ⊢ φ ∧ s ∈ 𝒫 B → I D K
24 4 adantr ⊢ φ ∧ s ∈ 𝒫 B → X ∈ B
25 simpr ⊢ φ ∧ s ∈ 𝒫 B → s ∈ 𝒫 B
26 1 2 23 24 25 ntrclselnel2 ⊢ φ ∧ s ∈ 𝒫 B → X ∈ I ⁡ B ∖ s ↔ ¬ X ∈ K ⁡ s
27 26 3adant3 ⊢ φ ∧ s ∈ 𝒫 B ∧ t = B ∖ s → X ∈ I ⁡ B ∖ s ↔ ¬ X ∈ K ⁡ s
28 22 27 bitrd ⊢ φ ∧ s ∈ 𝒫 B ∧ t = B ∖ s → X ∈ I ⁡ t ↔ ¬ X ∈ K ⁡ s
29 9 19 28 rexxfrd2 ⊢ φ → ∃ t ∈ 𝒫 B X ∈ I ⁡ t ↔ ∃ s ∈ 𝒫 B ¬ X ∈ K ⁡ s
30 7 29 syl5bb ⊢ φ → ∃ s ∈ 𝒫 B X ∈ I ⁡ s ↔ ∃ s ∈ 𝒫 B ¬ X ∈ K ⁡ s