Theorem clsneicnv

Description: If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the H operator, then the converse of the operator is known. (Contributed by RP, 5-Jun-2021)

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

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	5	cnveqi	⊢ ◡ 𝐻 = ◡ ( 𝐹 ∘ 𝐷 )
8		cnvco	⊢ ◡ ( 𝐹 ∘ 𝐷 ) = ( ◡ 𝐷 ∘ ◡ 𝐹 )
9	7 8	eqtri	⊢ ◡ 𝐻 = ( ◡ 𝐷 ∘ ◡ 𝐹 )
10	3 5 6	clsneibex	⊢ ( 𝜑 → 𝐵 ∈ V )
11		simpr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐵 ∈ V )
12	2 3 11	dssmapnvod	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → ◡ 𝐷 = 𝐷 )
13		pwexg	⊢ ( 𝐵 ∈ V → 𝒫 𝐵 ∈ V )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝒫 𝐵 ∈ V )
15		eqid	⊢ ( 𝐵 𝑂 𝒫 𝐵 ) = ( 𝐵 𝑂 𝒫 𝐵 )
16	1 14 11 4 15	fsovcnvd	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → ◡ 𝐹 = ( 𝐵 𝑂 𝒫 𝐵 ) )
17	12 16	coeq12d	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → ( ◡ 𝐷 ∘ ◡ 𝐹 ) = ( 𝐷 ∘ ( 𝐵 𝑂 𝒫 𝐵 ) ) )
18	10 17	mpdan	⊢ ( 𝜑 → ( ◡ 𝐷 ∘ ◡ 𝐹 ) = ( 𝐷 ∘ ( 𝐵 𝑂 𝒫 𝐵 ) ) )
19	9 18	syl5eq	⊢ ( 𝜑 → ◡ 𝐻 = ( 𝐷 ∘ ( 𝐵 𝑂 𝒫 𝐵 ) ) )