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 ⊢O=i∈V,j∈V⟼k∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m
clsnei.p ⊢P=n∈V⟼p∈𝒫n𝒫n⟼o∈𝒫n⟼n∖p⁡n∖o
clsnei.d ⊢D=P⁡B
clsnei.f ⊢F=𝒫BOB
clsnei.h ⊢H=F∘D
clsnei.r ⊢φ→KHN
Assertion clsneif1o ⊢φ→H:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB

Proof

Step Hyp Ref Expression
1 clsnei.o ⊢O=i∈V,j∈V⟼k∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m
2 clsnei.p ⊢P=n∈V⟼p∈𝒫n𝒫n⟼o∈𝒫n⟼n∖p⁡n∖o
3 clsnei.d ⊢D=P⁡B
4 clsnei.f ⊢F=𝒫BOB
5 clsnei.h ⊢H=F∘D
6 clsnei.r ⊢φ→KHN
7 3 5 6 clsneibex ⊢φ→B∈V
8 pwexg ⊢B∈V→𝒫B∈V
9 8 adantl ⊢φ∧B∈V→𝒫B∈V
10 simpr ⊢φ∧B∈V→B∈V
11 eqid ⊢𝒫BOB=𝒫BOB
12 1 9 10 11 fsovf1od ⊢φ∧B∈V→𝒫BOB:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB
13 eqid ⊢P⁡B=P⁡B
14 2 13 10 dssmapf1od ⊢φ∧B∈V→P⁡B:𝒫B𝒫B⟶1-1 onto𝒫B𝒫B
15 f1oco ⊢𝒫BOB:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB∧P⁡B:𝒫B𝒫B⟶1-1 onto𝒫B𝒫B→𝒫BOB∘P⁡B:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB
16 12 14 15 syl2anc ⊢φ∧B∈V→𝒫BOB∘P⁡B:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB
17 7 16 mpdan ⊢φ→𝒫BOB∘P⁡B:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB
18 4 3 coeq12i ⊢F∘D=𝒫BOB∘P⁡B
19 5 18 eqtri ⊢H=𝒫BOB∘P⁡B
20 f1oeq1 ⊢H=𝒫BOB∘P⁡B→H:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB↔𝒫BOB∘P⁡B:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB
21 19 20 ax-mp ⊢H:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB↔𝒫BOB∘P⁡B:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB
22 17 21 sylibr ⊢φ→H:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB