Theorem clsneifv4

Description: Value of the closure (interior) function in terms of the neighborhoods (convergents) function. (Contributed by RP, 27-Jun-2021)

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

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		clsneifv.s	⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
8		dfin5	⊢ ( 𝐵 ∩ ( 𝐾 ‘ 𝑆 ) ) = { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ ( 𝐾 ‘ 𝑆 ) }
9	1 2 3 4 5 6	clsneikex	⊢ ( 𝜑 → 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
10		elmapi	⊢ ( 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐾 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
11	9 10	syl	⊢ ( 𝜑 → 𝐾 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
12	11 7	ffvelrnd	⊢ ( 𝜑 → ( 𝐾 ‘ 𝑆 ) ∈ 𝒫 𝐵 )
13	12	elpwid	⊢ ( 𝜑 → ( 𝐾 ‘ 𝑆 ) ⊆ 𝐵 )
14		sseqin2	⊢ ( ( 𝐾 ‘ 𝑆 ) ⊆ 𝐵 ↔ ( 𝐵 ∩ ( 𝐾 ‘ 𝑆 ) ) = ( 𝐾 ‘ 𝑆 ) )
15	13 14	sylib	⊢ ( 𝜑 → ( 𝐵 ∩ ( 𝐾 ‘ 𝑆 ) ) = ( 𝐾 ‘ 𝑆 ) )
16	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐾 𝐻 𝑁 )
17		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
18	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑆 ∈ 𝒫 𝐵 )
19	1 2 3 4 5 16 17 18	clsneiel1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐾 ‘ 𝑆 ) ↔ ¬ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑁 ‘ 𝑥 ) ) )
20	19	rabbidva	⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ ( 𝐾 ‘ 𝑆 ) } = { 𝑥 ∈ 𝐵 ∣ ¬ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑁 ‘ 𝑥 ) } )
21	8 15 20	3eqtr3a	⊢ ( 𝜑 → ( 𝐾 ‘ 𝑆 ) = { 𝑥 ∈ 𝐵 ∣ ¬ ( 𝐵 ∖ 𝑆 ) ∈ ( 𝑁 ‘ 𝑥 ) } )