Metamath Proof Explorer

Theorem ntrclsfv1

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then there is a functional relation between them (Contributed by RP, 28-May-2021)

Ref Expression
Hypotheses ntrcls.o ⊢ O = i ∈ V ⟼ k ∈ 𝒫 i 𝒫 i ⟼ j ∈ 𝒫 i ⟼ i ∖ k ⁡ i ∖ j
ntrcls.d ⊢ D = O ⁡ B
ntrcls.r ⊢ φ → I D K
Assertion ntrclsfv1 ⊢ φ → D ⁡ I = K

Proof

Step Hyp Ref Expression
1 ntrcls.o ⊢ O = i ∈ V ⟼ k ∈ 𝒫 i 𝒫 i ⟼ j ∈ 𝒫 i ⟼ i ∖ k ⁡ i ∖ j
2 ntrcls.d ⊢ D = O ⁡ B
3 ntrcls.r ⊢ φ → I D K
4 1 2 3 ntrclsf1o ⊢ φ → D : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 B 𝒫 B
5 f1ofn ⊢ D : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 B 𝒫 B → D Fn 𝒫 B 𝒫 B
6 4 5 syl ⊢ φ → D Fn 𝒫 B 𝒫 B
7 1 2 3 ntrclsiex ⊢ φ → I ∈ 𝒫 B 𝒫 B
8 6 7 jca ⊢ φ → D Fn 𝒫 B 𝒫 B ∧ I ∈ 𝒫 B 𝒫 B
9 fnfun ⊢ D Fn 𝒫 B 𝒫 B → Fun ⁡ D
10 9 adantr ⊢ D Fn 𝒫 B 𝒫 B ∧ I ∈ 𝒫 B 𝒫 B → Fun ⁡ D
11 fndm ⊢ D Fn 𝒫 B 𝒫 B → dom ⁡ D = 𝒫 B 𝒫 B
12 11 eleq2d ⊢ D Fn 𝒫 B 𝒫 B → I ∈ dom ⁡ D ↔ I ∈ 𝒫 B 𝒫 B
13 12 biimpar ⊢ D Fn 𝒫 B 𝒫 B ∧ I ∈ 𝒫 B 𝒫 B → I ∈ dom ⁡ D
14 10 13 jca ⊢ D Fn 𝒫 B 𝒫 B ∧ I ∈ 𝒫 B 𝒫 B → Fun ⁡ D ∧ I ∈ dom ⁡ D
15 8 14 syl ⊢ φ → Fun ⁡ D ∧ I ∈ dom ⁡ D
16 funbrfvb ⊢ Fun ⁡ D ∧ I ∈ dom ⁡ D → D ⁡ I = K ↔ I D K
17 15 16 syl ⊢ φ → D ⁡ I = K ↔ I D K
18 3 17 mpbird ⊢ φ → D ⁡ I = K