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	$$⊢O=\left(i\in \mathrm{V},j\in \mathrm{V}⟼\left(k\in \left({𝒫j}^i\right)⟼\left(l\in j⟼\left\{m\in i|l\in k\left(m\right)\right\}\right)\right)\right)$$
	neicvg.p	$$⊢P=\left(n\in \mathrm{V}⟼\left(p\in \left({𝒫n}^{𝒫n}\right)⟼\left(o\in 𝒫n⟼n\setminus p\left(n\setminus o\right)\right)\right)\right)$$
	neicvg.d	$$⊢D=P\left(B\right)$$
	neicvg.f	$$⊢F=𝒫BOB$$
	neicvg.g	$$⊢G=BO𝒫B$$
	neicvg.h	$$⊢H=F\circ \left(D\circ G\right)$$
	neicvg.r	$$⊢\phi \to NHM$$
Assertion	neicvgnvo	$$⊢\phi \to H^{-1}=H$$

Proof

Step	Hyp	Ref	Expression
1		neicvg.o	$$⊢O=\left(i\in \mathrm{V},j\in \mathrm{V}⟼\left(k\in \left({𝒫j}^i\right)⟼\left(l\in j⟼\left\{m\in i|l\in k\left(m\right)\right\}\right)\right)\right)$$
2		neicvg.p	$$⊢P=\left(n\in \mathrm{V}⟼\left(p\in \left({𝒫n}^{𝒫n}\right)⟼\left(o\in 𝒫n⟼n\setminus p\left(n\setminus o\right)\right)\right)\right)$$
3		neicvg.d	$$⊢D=P\left(B\right)$$
4		neicvg.f	$$⊢F=𝒫BOB$$
5		neicvg.g	$$⊢G=BO𝒫B$$
6		neicvg.h	$$⊢H=F\circ \left(D\circ G\right)$$
7		neicvg.r	$$⊢\phi \to NHM$$
8	6	cnveqi	$$⊢H^{-1}={\left(F\circ \left(D\circ G\right)\right)}^{-1}$$
9		cnvco	$$⊢{\left(F\circ \left(D\circ G\right)\right)}^{-1}={\left(D\circ G\right)}^{-1}\circ F^{-1}$$
10		cnvco	$$⊢{\left(D\circ G\right)}^{-1}=G^{-1}\circ D^{-1}$$
11	10	coeq1i	$$⊢{\left(D\circ G\right)}^{-1}\circ F^{-1}=\left(G^{-1}\circ D^{-1}\right)\circ F^{-1}$$
12	8 9 11	3eqtri	$$⊢H^{-1}=\left(G^{-1}\circ D^{-1}\right)\circ F^{-1}$$
13	3 6 7	neicvgbex	$$⊢\phi \to B\in \mathrm{V}$$
14	13	pwexd	$$⊢\phi \to 𝒫B\in \mathrm{V}$$
15	1 13 14 5 4	fsovcnvd	$$⊢\phi \to G^{-1}=F$$
16	2 3 13	dssmapnvod	$$⊢\phi \to D^{-1}=D$$
17	15 16	coeq12d	$$⊢\phi \to G^{-1}\circ D^{-1}=F\circ D$$
18	1 14 13 4 5	fsovcnvd	$$⊢\phi \to F^{-1}=G$$
19	17 18	coeq12d	$$⊢\phi \to \left(G^{-1}\circ D^{-1}\right)\circ F^{-1}=\left(F\circ D\right)\circ G$$
20	12 19	eqtrid	$$⊢\phi \to H^{-1}=\left(F\circ D\right)\circ G$$
21		coass	$$⊢\left(F\circ D\right)\circ G=F\circ \left(D\circ G\right)$$
22	21 6	eqtr4i	$$⊢\left(F\circ D\right)\circ G=H$$
23	20 22	eqtrdi	$$⊢\phi \to H^{-1}=H$$