Theorem neicvgf1o

Description: If neighborhood and convergent functions are related by operator H , it is a one-to-one onto relation. (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	neicvgf1o	⊢ ( 𝜑 → 𝐻 : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )

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	3 6 7	neicvgbex	⊢ ( 𝜑 → 𝐵 ∈ V )
9	8	pwexd	⊢ ( 𝜑 → 𝒫 𝐵 ∈ V )
10	1 9 8 4	fsovf1od	⊢ ( 𝜑 → 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
11	2 3 8	dssmapf1od	⊢ ( 𝜑 → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
12	1 8 9 5	fsovf1od	⊢ ( 𝜑 → 𝐺 : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
13		f1oco	⊢ ( ( 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐺 : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( 𝐷 ∘ 𝐺 ) : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
14	11 12 13	syl2anc	⊢ ( 𝜑 → ( 𝐷 ∘ 𝐺 ) : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
15		f1oco	⊢ ( ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ∧ ( 𝐷 ∘ 𝐺 ) : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) ) : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
16	10 14 15	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) ) : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
17		f1oeq1	⊢ ( 𝐻 = ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) ) → ( 𝐻 : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ↔ ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) ) : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ) )
18	6 17	ax-mp	⊢ ( 𝐻 : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ↔ ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) ) : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
19	16 18	sylibr	⊢ ( 𝜑 → 𝐻 : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )