Metamath Proof Explorer

Theorem dssmapntrcls

Description: The interior and closure operators on a topology are duals of each other. See also kur14lem2 . (Contributed by RP, 21-Apr-2021)

Ref Expression
Hypotheses dssmapclsntr.x ⊢ X = ⋃ J
dssmapclsntr.k ⊢ K = cls ⁡ J
dssmapclsntr.i ⊢ I = int ⁡ J
dssmapclsntr.o ⊢ O = b ∈ V ⟼ f ∈ 𝒫 b 𝒫 b ⟼ s ∈ 𝒫 b ⟼ b ∖ f ⁡ b ∖ s
dssmapclsntr.d ⊢ D = O ⁡ X
Assertion dssmapntrcls ⊢ J ∈ Top → I = D ⁡ K

Proof

Step Hyp Ref Expression
1 dssmapclsntr.x ⊢ X = ⋃ J
2 dssmapclsntr.k ⊢ K = cls ⁡ J
3 dssmapclsntr.i ⊢ I = int ⁡ J
4 dssmapclsntr.o ⊢ O = b ∈ V ⟼ f ∈ 𝒫 b 𝒫 b ⟼ s ∈ 𝒫 b ⟼ b ∖ f ⁡ b ∖ s
5 dssmapclsntr.d ⊢ D = O ⁡ X
6 vpwex ⊢ 𝒫 t ∈ V
7 6 inex2 ⊢ J ∩ 𝒫 t ∈ V
8 7 uniex ⊢ ⋃ J ∩ 𝒫 t ∈ V
9 8 rgenw ⊢ ∀ t ∈ 𝒫 X ⋃ J ∩ 𝒫 t ∈ V
10 nfcv ⊢ Ⅎ _ t 𝒫 X
11 10 fnmptf ⊢ ∀ t ∈ 𝒫 X ⋃ J ∩ 𝒫 t ∈ V → t ∈ 𝒫 X ⟼ ⋃ J ∩ 𝒫 t Fn 𝒫 X
12 9 11 mp1i ⊢ J ∈ Top → t ∈ 𝒫 X ⟼ ⋃ J ∩ 𝒫 t Fn 𝒫 X
13 1 ntrfval ⊢ J ∈ Top → int ⁡ J = t ∈ 𝒫 X ⟼ ⋃ J ∩ 𝒫 t
14 3 13 eqtrid ⊢ J ∈ Top → I = t ∈ 𝒫 X ⟼ ⋃ J ∩ 𝒫 t
15 14 fneq1d ⊢ J ∈ Top → I Fn 𝒫 X ↔ t ∈ 𝒫 X ⟼ ⋃ J ∩ 𝒫 t Fn 𝒫 X
16 12 15 mpbird ⊢ J ∈ Top → I Fn 𝒫 X
17 1 topopn ⊢ J ∈ Top → X ∈ J
18 4 5 17 dssmapf1od ⊢ J ∈ Top → D : 𝒫 X 𝒫 X ⟶ 1-1 onto 𝒫 X 𝒫 X
19 f1of ⊢ D : 𝒫 X 𝒫 X ⟶ 1-1 onto 𝒫 X 𝒫 X → D : 𝒫 X 𝒫 X ⟶ 𝒫 X 𝒫 X
20 18 19 syl ⊢ J ∈ Top → D : 𝒫 X 𝒫 X ⟶ 𝒫 X 𝒫 X
21 1 2 clselmap ⊢ J ∈ Top → K ∈ 𝒫 X 𝒫 X
22 20 21 ffvelcdmd ⊢ J ∈ Top → D ⁡ K ∈ 𝒫 X 𝒫 X
23 elmapfn ⊢ D ⁡ K ∈ 𝒫 X 𝒫 X → D ⁡ K Fn 𝒫 X
24 22 23 syl ⊢ J ∈ Top → D ⁡ K Fn 𝒫 X
25 elpwi ⊢ t ∈ 𝒫 X → t ⊆ X
26 1 ntrval2 ⊢ J ∈ Top ∧ t ⊆ X → int ⁡ J ⁡ t = X ∖ cls ⁡ J ⁡ X ∖ t
27 25 26 sylan2 ⊢ J ∈ Top ∧ t ∈ 𝒫 X → int ⁡ J ⁡ t = X ∖ cls ⁡ J ⁡ X ∖ t
28 3 fveq1i ⊢ I ⁡ t = int ⁡ J ⁡ t
29 2 fveq1i ⊢ K ⁡ X ∖ t = cls ⁡ J ⁡ X ∖ t
30 29 difeq2i ⊢ X ∖ K ⁡ X ∖ t = X ∖ cls ⁡ J ⁡ X ∖ t
31 27 28 30 3eqtr4g ⊢ J ∈ Top ∧ t ∈ 𝒫 X → I ⁡ t = X ∖ K ⁡ X ∖ t
32 17 adantr ⊢ J ∈ Top ∧ t ∈ 𝒫 X → X ∈ J
33 21 adantr ⊢ J ∈ Top ∧ t ∈ 𝒫 X → K ∈ 𝒫 X 𝒫 X
34 eqid ⊢ D ⁡ K = D ⁡ K
35 simpr ⊢ J ∈ Top ∧ t ∈ 𝒫 X → t ∈ 𝒫 X
36 eqid ⊢ D ⁡ K ⁡ t = D ⁡ K ⁡ t
37 4 5 32 33 34 35 36 dssmapfv3d ⊢ J ∈ Top ∧ t ∈ 𝒫 X → D ⁡ K ⁡ t = X ∖ K ⁡ X ∖ t
38 31 37 eqtr4d ⊢ J ∈ Top ∧ t ∈ 𝒫 X → I ⁡ t = D ⁡ K ⁡ t
39 16 24 38 eqfnfvd ⊢ J ∈ Top → I = D ⁡ K