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 ∈ 𝒫 j i ⟼ 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 = 𝒫 B O B
clsnei.h ⊢ H = F ∘ D
clsnei.r ⊢ φ → K H N
Assertion clsneif1o ⊢ φ → H : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B

Proof

Step Hyp Ref Expression
1 clsnei.o ⊢ O = i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ 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 = 𝒫 B O B
5 clsnei.h ⊢ H = F ∘ D
6 clsnei.r ⊢ φ → K H N
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 ⊢ 𝒫 B O B = 𝒫 B O B
12 1 9 10 11 fsovf1od ⊢ φ ∧ B ∈ V → 𝒫 B O B : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B
13 eqid ⊢ P ⁡ B = P ⁡ B
14 2 13 10 dssmapf1od ⊢ φ ∧ B ∈ V → P ⁡ B : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 B 𝒫 B
15 f1oco ⊢ 𝒫 B O B : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B ∧ P ⁡ B : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 B 𝒫 B → 𝒫 B O B ∘ P ⁡ B : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B
16 12 14 15 syl2anc ⊢ φ ∧ B ∈ V → 𝒫 B O B ∘ P ⁡ B : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B
17 7 16 mpdan ⊢ φ → 𝒫 B O B ∘ P ⁡ B : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B
18 4 3 coeq12i ⊢ F ∘ D = 𝒫 B O B ∘ P ⁡ B
19 5 18 eqtri ⊢ H = 𝒫 B O B ∘ P ⁡ B
20 f1oeq1 ⊢ H = 𝒫 B O B ∘ P ⁡ B → H : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B ↔ 𝒫 B O B ∘ P ⁡ B : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B
21 19 20 ax-mp ⊢ H : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B ↔ 𝒫 B O B ∘ P ⁡ B : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B
22 17 21 sylibr ⊢ φ → H : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B