Metamath Proof Explorer

Theorem clsneif1o

Description: If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the H operator, then the operator is a one-to-one, onto mapping. (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 clsneif1o ( 𝜑 → 𝐻 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )

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 3 5 6 clsneibex ⊢ ( 𝜑 → 𝐵 ∈ V )
8 pwexg ⊢ ( 𝐵 ∈ V → 𝒫 𝐵 ∈ V )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝒫 𝐵 ∈ V )
10 simpr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐵 ∈ V )
11 eqid ⊢ ( 𝒫 𝐵 𝑂 𝐵 ) = ( 𝒫 𝐵 𝑂 𝐵 )
12 1 9 10 11 fsovf1od ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → ( 𝒫 𝐵 𝑂 𝐵 ) : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
13 eqid ⊢ ( 𝑃 ‘ 𝐵 ) = ( 𝑃 ‘ 𝐵 )
14 2 13 10 dssmapf1od ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → ( 𝑃 ‘ 𝐵 ) : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
15 f1oco ⊢ ( ( ( 𝒫 𝐵 𝑂 𝐵 ) : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ∧ ( 𝑃 ‘ 𝐵 ) : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( ( 𝒫 𝐵 𝑂 𝐵 ) ∘ ( 𝑃 ‘ 𝐵 ) ) : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
16 12 14 15 syl2anc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → ( ( 𝒫 𝐵 𝑂 𝐵 ) ∘ ( 𝑃 ‘ 𝐵 ) ) : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
17 7 16 mpdan ⊢ ( 𝜑 → ( ( 𝒫 𝐵 𝑂 𝐵 ) ∘ ( 𝑃 ‘ 𝐵 ) ) : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
18 4 3 coeq12i ⊢ ( 𝐹 ∘ 𝐷 ) = ( ( 𝒫 𝐵 𝑂 𝐵 ) ∘ ( 𝑃 ‘ 𝐵 ) )
19 5 18 eqtri ⊢ 𝐻 = ( ( 𝒫 𝐵 𝑂 𝐵 ) ∘ ( 𝑃 ‘ 𝐵 ) )
20 f1oeq1 ⊢ ( 𝐻 = ( ( 𝒫 𝐵 𝑂 𝐵 ) ∘ ( 𝑃 ‘ 𝐵 ) ) → ( 𝐻 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ↔ ( ( 𝒫 𝐵 𝑂 𝐵 ) ∘ ( 𝑃 ‘ 𝐵 ) ) : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ) )
21 19 20 ax-mp ⊢ ( 𝐻 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ↔ ( ( 𝒫 𝐵 𝑂 𝐵 ) ∘ ( 𝑃 ‘ 𝐵 ) ) : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
22 17 21 sylibr ⊢ ( 𝜑 → 𝐻 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )