Theorem neicvgnvo

Description: If neighborhood and convergent functions are related by operator H , it is its own converse function. (Contributed by RP, 11-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		neicvg.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		neicvg.p	⊢ 𝑃 = ( 𝑛 ∈ V ↦ ( 𝑝 ∈ ( 𝒫 𝑛 ↑m 𝒫 𝑛 ) ↦ ( 𝑜 ∈ 𝒫 𝑛 ↦ ( 𝑛 ∖ ( 𝑝 ‘ ( 𝑛 ∖ 𝑜 ) ) ) ) ) )
3		neicvg.d	⊢ 𝐷 = ( 𝑃 ‘ 𝐵 )
4		neicvg.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
5		neicvg.g	⊢ 𝐺 = ( 𝐵 𝑂 𝒫 𝐵 )
6		neicvg.h	⊢ 𝐻 = ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) )
7		neicvg.r	⊢ ( 𝜑 → 𝑁 𝐻 𝑀 )
8	6	cnveqi	⊢ ◡ 𝐻 = ◡ ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) )
9		cnvco	⊢ ◡ ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) ) = ( ◡ ( 𝐷 ∘ 𝐺 ) ∘ ◡ 𝐹 )
10		cnvco	⊢ ◡ ( 𝐷 ∘ 𝐺 ) = ( ◡ 𝐺 ∘ ◡ 𝐷 )
11	10	coeq1i	⊢ ( ◡ ( 𝐷 ∘ 𝐺 ) ∘ ◡ 𝐹 ) = ( ( ◡ 𝐺 ∘ ◡ 𝐷 ) ∘ ◡ 𝐹 )
12	8 9 11	3eqtri	⊢ ◡ 𝐻 = ( ( ◡ 𝐺 ∘ ◡ 𝐷 ) ∘ ◡ 𝐹 )
13	3 6 7	neicvgbex	⊢ ( 𝜑 → 𝐵 ∈ V )
14	13	pwexd	⊢ ( 𝜑 → 𝒫 𝐵 ∈ V )
15	1 13 14 5 4	fsovcnvd	⊢ ( 𝜑 → ◡ 𝐺 = 𝐹 )
16	2 3 13	dssmapnvod	⊢ ( 𝜑 → ◡ 𝐷 = 𝐷 )
17	15 16	coeq12d	⊢ ( 𝜑 → ( ◡ 𝐺 ∘ ◡ 𝐷 ) = ( 𝐹 ∘ 𝐷 ) )
18	1 14 13 4 5	fsovcnvd	⊢ ( 𝜑 → ◡ 𝐹 = 𝐺 )
19	17 18	coeq12d	⊢ ( 𝜑 → ( ( ◡ 𝐺 ∘ ◡ 𝐷 ) ∘ ◡ 𝐹 ) = ( ( 𝐹 ∘ 𝐷 ) ∘ 𝐺 ) )
20	12 19	syl5eq	⊢ ( 𝜑 → ◡ 𝐻 = ( ( 𝐹 ∘ 𝐷 ) ∘ 𝐺 ) )
21		coass	⊢ ( ( 𝐹 ∘ 𝐷 ) ∘ 𝐺 ) = ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) )
22	21 6	eqtr4i	⊢ ( ( 𝐹 ∘ 𝐷 ) ∘ 𝐺 ) = 𝐻
23	20 22	eqtrdi	⊢ ( 𝜑 → ◡ 𝐻 = 𝐻 )