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 ⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
ntrcls.d ⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
ntrcls.r ⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
ntrclslem0.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion ntrclsneine0lem ( 𝜑 → ( ∃ 𝑠 ∈ 𝒫 𝐵 𝑋 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ∃ 𝑠 ∈ 𝒫 𝐵 ¬ 𝑋 ∈ ( 𝐾 ‘ 𝑠 ) ) )

Proof

Step Hyp Ref Expression
1 ntrcls.o ⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
2 ntrcls.d ⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
3 ntrcls.r ⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
4 ntrclslem0.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 fveq2 ⊢ ( 𝑠 = 𝑡 → ( 𝐼 ‘ 𝑠 ) = ( 𝐼 ‘ 𝑡 ) )
6 5 eleq2d ⊢ ( 𝑠 = 𝑡 → ( 𝑋 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑋 ∈ ( 𝐼 ‘ 𝑡 ) ) )
7 6 cbvrexvw ⊢ ( ∃ 𝑠 ∈ 𝒫 𝐵 𝑋 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ∃ 𝑡 ∈ 𝒫 𝐵 𝑋 ∈ ( 𝐼 ‘ 𝑡 ) )
8 2 3 ntrclsrcomplex ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑠 ) ∈ 𝒫 𝐵 )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑠 ) ∈ 𝒫 𝐵 )
10 2 3 ntrclsrcomplex ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑡 ) ∈ 𝒫 𝐵 )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑡 ) ∈ 𝒫 𝐵 )
12 difeq2 ⊢ ( 𝑠 = ( 𝐵 ∖ 𝑡 ) → ( 𝐵 ∖ 𝑠 ) = ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) )
13 12 adantl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑠 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐵 ∖ 𝑠 ) = ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) )
14 elpwi ⊢ ( 𝑡 ∈ 𝒫 𝐵 → 𝑡 ⊆ 𝐵 )
15 dfss4 ⊢ ( 𝑡 ⊆ 𝐵 ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) = 𝑡 )
16 14 15 sylib ⊢ ( 𝑡 ∈ 𝒫 𝐵 → ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) = 𝑡 )
17 16 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑠 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) = 𝑡 )
18 13 17 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑠 = ( 𝐵 ∖ 𝑡 ) ) → 𝑡 = ( 𝐵 ∖ 𝑠 ) )
19 11 18 rspcedeq2vd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ∃ 𝑠 ∈ 𝒫 𝐵 𝑡 = ( 𝐵 ∖ 𝑠 ) )
20 fveq2 ⊢ ( 𝑡 = ( 𝐵 ∖ 𝑠 ) → ( 𝐼 ‘ 𝑡 ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) )
21 20 eleq2d ⊢ ( 𝑡 = ( 𝐵 ∖ 𝑠 ) → ( 𝑋 ∈ ( 𝐼 ‘ 𝑡 ) ↔ 𝑋 ∈ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
22 21 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( 𝑋 ∈ ( 𝐼 ‘ 𝑡 ) ↔ 𝑋 ∈ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
23 3 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝐼 𝐷 𝐾 )
24 4 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑋 ∈ 𝐵 )
25 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
26 1 2 23 24 25 ntrclselnel2 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝑋 ∈ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ↔ ¬ 𝑋 ∈ ( 𝐾 ‘ 𝑠 ) ) )
27 26 3adant3 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( 𝑋 ∈ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ↔ ¬ 𝑋 ∈ ( 𝐾 ‘ 𝑠 ) ) )
28 22 27 bitrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( 𝑋 ∈ ( 𝐼 ‘ 𝑡 ) ↔ ¬ 𝑋 ∈ ( 𝐾 ‘ 𝑠 ) ) )
29 9 19 28 rexxfrd2 ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ 𝒫 𝐵 𝑋 ∈ ( 𝐼 ‘ 𝑡 ) ↔ ∃ 𝑠 ∈ 𝒫 𝐵 ¬ 𝑋 ∈ ( 𝐾 ‘ 𝑠 ) ) )
30 7 29 bitrid ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝒫 𝐵 𝑋 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ∃ 𝑠 ∈ 𝒫 𝐵 ¬ 𝑋 ∈ ( 𝐾 ‘ 𝑠 ) ) )