Theorem ntrneineine0lem

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

	Ref	Expression
Hypotheses	ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
	ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
	ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
	ntrnei.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	ntrneineine0lem	⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝒫 𝐵 𝑋 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ( 𝑁 ‘ 𝑋 ) ≠ ∅ ) )

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	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝒫 𝐵 𝑋 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ∃ 𝑠 ∈ 𝒫 𝐵 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ) )
10	1 2 3	ntrneinex	⊢ ( 𝜑 → 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
11		elmapi	⊢ ( 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → 𝑁 : 𝐵 ⟶ 𝒫 𝒫 𝐵 )
12	10 11	syl	⊢ ( 𝜑 → 𝑁 : 𝐵 ⟶ 𝒫 𝒫 𝐵 )
13	12 4	ffvelcdmd	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ∈ 𝒫 𝒫 𝐵 )
14	13	elpwid	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ⊆ 𝒫 𝐵 )
15	14	sseld	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) → 𝑠 ∈ 𝒫 𝐵 ) )
16	15	pm4.71rd	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ↔ ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ) ) )
17	16	exbidv	⊢ ( 𝜑 → ( ∃ 𝑠 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ) ) )
18	17	bicomd	⊢ ( 𝜑 → ( ∃ 𝑠 ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ) ↔ ∃ 𝑠 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ) )
19		df-rex	⊢ ( ∃ 𝑠 ∈ 𝒫 𝐵 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ) )
20		n0	⊢ ( ( 𝑁 ‘ 𝑋 ) ≠ ∅ ↔ ∃ 𝑠 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) )
21	18 19 20	3bitr4g	⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝒫 𝐵 𝑠 ∈ ( 𝑁 ‘ 𝑋 ) ↔ ( 𝑁 ‘ 𝑋 ) ≠ ∅ ) )
22	9 21	bitrd	⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝒫 𝐵 𝑋 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ( 𝑁 ‘ 𝑋 ) ≠ ∅ ) )