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

Proof

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

Metamath Proof Explorer

Theorem neicvgnvo

Proof