Theorem ntrneicls11

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then conditions equal to claiming that the interior of the empty set is the empty set hold equally. (Contributed by RP, 2-Jun-2021)

	Ref	Expression
Hypotheses	ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
	ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
	ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
Assertion	ntrneicls11	⊢ ( 𝜑 → ( ( 𝐼 ‘ ∅ ) = ∅ ↔ ∀ 𝑥 ∈ 𝐵 ¬ ∅ ∈ ( 𝑁 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3		ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4	1 2 3	ntrneiiex	⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
5		elmapi	⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
6	4 5	syl	⊢ ( 𝜑 → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
7		0elpw	⊢ ∅ ∈ 𝒫 𝐵
8	7	a1i	⊢ ( 𝜑 → ∅ ∈ 𝒫 𝐵 )
9	6 8	ffvelcdmd	⊢ ( 𝜑 → ( 𝐼 ‘ ∅ ) ∈ 𝒫 𝐵 )
10	9	elpwid	⊢ ( 𝜑 → ( 𝐼 ‘ ∅ ) ⊆ 𝐵 )
11		reldisj	⊢ ( ( 𝐼 ‘ ∅ ) ⊆ 𝐵 → ( ( ( 𝐼 ‘ ∅ ) ∩ 𝐵 ) = ∅ ↔ ( 𝐼 ‘ ∅ ) ⊆ ( 𝐵 ∖ 𝐵 ) ) )
12	10 11	syl	⊢ ( 𝜑 → ( ( ( 𝐼 ‘ ∅ ) ∩ 𝐵 ) = ∅ ↔ ( 𝐼 ‘ ∅ ) ⊆ ( 𝐵 ∖ 𝐵 ) ) )
13	12	bicomd	⊢ ( 𝜑 → ( ( 𝐼 ‘ ∅ ) ⊆ ( 𝐵 ∖ 𝐵 ) ↔ ( ( 𝐼 ‘ ∅ ) ∩ 𝐵 ) = ∅ ) )
14		difid	⊢ ( 𝐵 ∖ 𝐵 ) = ∅
15	14	sseq2i	⊢ ( ( 𝐼 ‘ ∅ ) ⊆ ( 𝐵 ∖ 𝐵 ) ↔ ( 𝐼 ‘ ∅ ) ⊆ ∅ )
16		ss0b	⊢ ( ( 𝐼 ‘ ∅ ) ⊆ ∅ ↔ ( 𝐼 ‘ ∅ ) = ∅ )
17	15 16	bitri	⊢ ( ( 𝐼 ‘ ∅ ) ⊆ ( 𝐵 ∖ 𝐵 ) ↔ ( 𝐼 ‘ ∅ ) = ∅ )
18		disjr	⊢ ( ( ( 𝐼 ‘ ∅ ) ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝐼 ‘ ∅ ) )
19	13 17 18	3bitr3g	⊢ ( 𝜑 → ( ( 𝐼 ‘ ∅ ) = ∅ ↔ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝐼 ‘ ∅ ) ) )
20	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐼 𝐹 𝑁 )
21		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
22	7	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∅ ∈ 𝒫 𝐵 )
23	1 2 20 21 22	ntrneiel	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ ∅ ) ↔ ∅ ∈ ( 𝑁 ‘ 𝑥 ) ) )
24	23	notbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ¬ 𝑥 ∈ ( 𝐼 ‘ ∅ ) ↔ ¬ ∅ ∈ ( 𝑁 ‘ 𝑥 ) ) )
25	24	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝐼 ‘ ∅ ) ↔ ∀ 𝑥 ∈ 𝐵 ¬ ∅ ∈ ( 𝑁 ‘ 𝑥 ) ) )
26	19 25	bitrd	⊢ ( 𝜑 → ( ( 𝐼 ‘ ∅ ) = ∅ ↔ ∀ 𝑥 ∈ 𝐵 ¬ ∅ ∈ ( 𝑁 ‘ 𝑥 ) ) )