Theorem clsneiel1

Description: If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the H operator, then membership in the closure of a subset is equivalent to the complement of the subset not being a neighborhood of the point. (Contributed by RP, 7-Jun-2021)

	Ref	Expression
Hypotheses	clsnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
	clsnei.p	⊢ 𝑃 = ( 𝑛 ∈ V ↦ ( 𝑝 ∈ ( 𝒫 𝑛 ↑m 𝒫 𝑛 ) ↦ ( 𝑜 ∈ 𝒫 𝑛 ↦ ( 𝑛 ∖ ( 𝑝 ‘ ( 𝑛 ∖ 𝑜 ) ) ) ) ) )
	clsnei.d	⊢ 𝐷 = ( 𝑃 ‘ 𝐵 )
	clsnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
	clsnei.h	⊢ 𝐻 = ( 𝐹 ∘ 𝐷 )
	clsnei.r	⊢ ( 𝜑 → 𝐾 𝐻 𝑁 )
	clsneiel.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	clsneiel.s	⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
Assertion	clsneiel1	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐾 ‘ 𝑆 ) ↔ ¬ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑁 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		clsnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		clsnei.p	⊢ 𝑃 = ( 𝑛 ∈ V ↦ ( 𝑝 ∈ ( 𝒫 𝑛 ↑m 𝒫 𝑛 ) ↦ ( 𝑜 ∈ 𝒫 𝑛 ↦ ( 𝑛 ∖ ( 𝑝 ‘ ( 𝑛 ∖ 𝑜 ) ) ) ) ) )
3		clsnei.d	⊢ 𝐷 = ( 𝑃 ‘ 𝐵 )
4		clsnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
5		clsnei.h	⊢ 𝐻 = ( 𝐹 ∘ 𝐷 )
6		clsnei.r	⊢ ( 𝜑 → 𝐾 𝐻 𝑁 )
7		clsneiel.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		clsneiel.s	⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
9	3 5 6	clsneibex	⊢ ( 𝜑 → 𝐵 ∈ V )
10	9	ancli	⊢ ( 𝜑 → ( 𝜑 ∧ 𝐵 ∈ V ) )
11		simpr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐵 ∈ V )
12	11	pwexd	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝒫 𝐵 ∈ V )
13	1 12 11 4	fsovfd	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ⟶ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
14	13	ffnd	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐹 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
15	2 3 11	dssmapf1od	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
16		f1of	⊢ ( 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ⟶ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
17	15 16	syl	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ⟶ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
18	5	breqi	⊢ ( 𝐾 𝐻 𝑁 ↔ 𝐾 ( 𝐹 ∘ 𝐷 ) 𝑁 )
19	6 18	sylib	⊢ ( 𝜑 → 𝐾 ( 𝐹 ∘ 𝐷 ) 𝑁 )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐾 ( 𝐹 ∘ 𝐷 ) 𝑁 )
21	14 17 20	brcoffn	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → ( 𝐾 𝐷 ( 𝐷 ‘ 𝐾 ) ∧ ( 𝐷 ‘ 𝐾 ) 𝐹 𝑁 ) )
22		simprl	⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝐾 𝐷 ( 𝐷 ‘ 𝐾 ) ∧ ( 𝐷 ‘ 𝐾 ) 𝐹 𝑁 ) ) → 𝐾 𝐷 ( 𝐷 ‘ 𝐾 ) )
23	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝐾 𝐷 ( 𝐷 ‘ 𝐾 ) ∧ ( 𝐷 ‘ 𝐾 ) 𝐹 𝑁 ) ) → 𝑋 ∈ 𝐵 )
24	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝐾 𝐷 ( 𝐷 ‘ 𝐾 ) ∧ ( 𝐷 ‘ 𝐾 ) 𝐹 𝑁 ) ) → 𝑆 ∈ 𝒫 𝐵 )
25	2 3 22 23 24	ntrclselnel1	⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝐾 𝐷 ( 𝐷 ‘ 𝐾 ) ∧ ( 𝐷 ‘ 𝐾 ) 𝐹 𝑁 ) ) → ( 𝑋 ∈ ( 𝐾 ‘ 𝑆 ) ↔ ¬ 𝑋 ∈ ( ( 𝐷 ‘ 𝐾 ) ‘ ( 𝐵 ∖ 𝑆 ) ) ) )
26		simprr	⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝐾 𝐷 ( 𝐷 ‘ 𝐾 ) ∧ ( 𝐷 ‘ 𝐾 ) 𝐹 𝑁 ) ) → ( 𝐷 ‘ 𝐾 ) 𝐹 𝑁 )
27		simplr	⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝐾 𝐷 ( 𝐷 ‘ 𝐾 ) ∧ ( 𝐷 ‘ 𝐾 ) 𝐹 𝑁 ) ) → 𝐵 ∈ V )
28		difssd	⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝐾 𝐷 ( 𝐷 ‘ 𝐾 ) ∧ ( 𝐷 ‘ 𝐾 ) 𝐹 𝑁 ) ) → ( 𝐵 ∖ 𝑆 ) ⊆ 𝐵 )
29	27 28	sselpwd	⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝐾 𝐷 ( 𝐷 ‘ 𝐾 ) ∧ ( 𝐷 ‘ 𝐾 ) 𝐹 𝑁 ) ) → ( 𝐵 ∖ 𝑆 ) ∈ 𝒫 𝐵 )
30	1 4 26 23 29	ntrneiel	⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝐾 𝐷 ( 𝐷 ‘ 𝐾 ) ∧ ( 𝐷 ‘ 𝐾 ) 𝐹 𝑁 ) ) → ( 𝑋 ∈ ( ( 𝐷 ‘ 𝐾 ) ‘ ( 𝐵 ∖ 𝑆 ) ) ↔ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑁 ‘ 𝑋 ) ) )
31	30	notbid	⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝐾 𝐷 ( 𝐷 ‘ 𝐾 ) ∧ ( 𝐷 ‘ 𝐾 ) 𝐹 𝑁 ) ) → ( ¬ 𝑋 ∈ ( ( 𝐷 ‘ 𝐾 ) ‘ ( 𝐵 ∖ 𝑆 ) ) ↔ ¬ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑁 ‘ 𝑋 ) ) )
32	25 31	bitrd	⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ V ) ∧ ( 𝐾 𝐷 ( 𝐷 ‘ 𝐾 ) ∧ ( 𝐷 ‘ 𝐾 ) 𝐹 𝑁 ) ) → ( 𝑋 ∈ ( 𝐾 ‘ 𝑆 ) ↔ ¬ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑁 ‘ 𝑋 ) ) )
33	10 21 32	syl2anc2	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐾 ‘ 𝑆 ) ↔ ¬ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑁 ‘ 𝑋 ) ) )