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 ⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
ntrnei.f ⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
ntrnei.r ⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
ntrnei.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion ntrneineine1lem ( 𝜑 → ( ∃ 𝑠 ∈ 𝒫 𝐵 ¬ 𝑋 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ( 𝑁 ‘ 𝑋 ) ≠ 𝒫 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ntrnei.o ⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2 ntrnei.f ⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3 ntrnei.r ⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4 ntrnei.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 3 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝐼 𝐹 𝑁 )
6 4 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑋 ∈ 𝐵 )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
8 1 2 5 6 7 ntrneiel ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝑋 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ) )
9 8 notbid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ¬ 𝑋 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ¬ 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ) )
10 9 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝒫 𝐵 ¬ 𝑋 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ∃ 𝑠 ∈ 𝒫 𝐵 ¬ 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ) )
11 1 2 3 ntrneinex ⊢ ( 𝜑 → 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
12 elmapi ⊢ ( 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → 𝑁 : 𝐵 ⟶ 𝒫 𝒫 𝐵 )
13 11 12 syl ⊢ ( 𝜑 → 𝑁 : 𝐵 ⟶ 𝒫 𝒫 𝐵 )
14 13 4 ffvelcdmd ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ∈ 𝒫 𝒫 𝐵 )
15 14 elpwid ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ⊆ 𝒫 𝐵 )
16 biortn ⊢ ( ( 𝑁 ‘ 𝑋 ) ⊆ 𝒫 𝐵 → ( ¬ 𝒫 𝐵 ⊆ ( 𝑁 ‘ 𝑋 ) ↔ ( ¬ ( 𝑁 ‘ 𝑋 ) ⊆ 𝒫 𝐵 ∨ ¬ 𝒫 𝐵 ⊆ ( 𝑁 ‘ 𝑋 ) ) ) )
17 15 16 syl ⊢ ( 𝜑 → ( ¬ 𝒫 𝐵 ⊆ ( 𝑁 ‘ 𝑋 ) ↔ ( ¬ ( 𝑁 ‘ 𝑋 ) ⊆ 𝒫 𝐵 ∨ ¬ 𝒫 𝐵 ⊆ ( 𝑁 ‘ 𝑋 ) ) ) )
18 df-rex ⊢ ( ∃ 𝑠 ∈ 𝒫 𝐵 ¬ 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝒫 𝐵 ∧ ¬ 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ) )
19 nss ⊢ ( ¬ 𝒫 𝐵 ⊆ ( 𝑁 ‘ 𝑋 ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝒫 𝐵 ∧ ¬ 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ) )
20 18 19 bitr4i ⊢ ( ∃ 𝑠 ∈ 𝒫 𝐵 ¬ 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ↔ ¬ 𝒫 𝐵 ⊆ ( 𝑁 ‘ 𝑋 ) )
21 df-ne ⊢ ( ( 𝑁 ‘ 𝑋 ) ≠ 𝒫 𝐵 ↔ ¬ ( 𝑁 ‘ 𝑋 ) = 𝒫 𝐵 )
22 ianor ⊢ ( ¬ ( ( 𝑁 ‘ 𝑋 ) ⊆ 𝒫 𝐵 ∧ 𝒫 𝐵 ⊆ ( 𝑁 ‘ 𝑋 ) ) ↔ ( ¬ ( 𝑁 ‘ 𝑋 ) ⊆ 𝒫 𝐵 ∨ ¬ 𝒫 𝐵 ⊆ ( 𝑁 ‘ 𝑋 ) ) )
23 eqss ⊢ ( ( 𝑁 ‘ 𝑋 ) = 𝒫 𝐵 ↔ ( ( 𝑁 ‘ 𝑋 ) ⊆ 𝒫 𝐵 ∧ 𝒫 𝐵 ⊆ ( 𝑁 ‘ 𝑋 ) ) )
24 22 23 xchnxbir ⊢ ( ¬ ( 𝑁 ‘ 𝑋 ) = 𝒫 𝐵 ↔ ( ¬ ( 𝑁 ‘ 𝑋 ) ⊆ 𝒫 𝐵 ∨ ¬ 𝒫 𝐵 ⊆ ( 𝑁 ‘ 𝑋 ) ) )
25 21 24 bitri ⊢ ( ( 𝑁 ‘ 𝑋 ) ≠ 𝒫 𝐵 ↔ ( ¬ ( 𝑁 ‘ 𝑋 ) ⊆ 𝒫 𝐵 ∨ ¬ 𝒫 𝐵 ⊆ ( 𝑁 ‘ 𝑋 ) ) )
26 17 20 25 3bitr4g ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝒫 𝐵 ¬ 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ↔ ( 𝑁 ‘ 𝑋 ) ≠ 𝒫 𝐵 ) )
27 10 26 bitrd ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝒫 𝐵 ¬ 𝑋 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ( 𝑁 ‘ 𝑋 ) ≠ 𝒫 𝐵 ) )