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 ⊢ 𝑋 = ∪ 𝐽
dssmapclsntr.k ⊢ 𝐾 = ( cls ‘ 𝐽 )
dssmapclsntr.i ⊢ 𝐼 = ( int ‘ 𝐽 )
dssmapclsntr.o ⊢ 𝑂 = ( 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝒫 𝑏 ) ↦ ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) ) ) ) )
dssmapclsntr.d ⊢ 𝐷 = ( 𝑂 ‘ 𝑋 )
Assertion dssmapntrcls ( 𝐽 ∈ Top → 𝐼 = ( 𝐷 ‘ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 dssmapclsntr.x ⊢ 𝑋 = ∪ 𝐽
2 dssmapclsntr.k ⊢ 𝐾 = ( cls ‘ 𝐽 )
3 dssmapclsntr.i ⊢ 𝐼 = ( int ‘ 𝐽 )
4 dssmapclsntr.o ⊢ 𝑂 = ( 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝒫 𝑏 ) ↦ ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) ) ) ) )
5 dssmapclsntr.d ⊢ 𝐷 = ( 𝑂 ‘ 𝑋 )
6 vpwex ⊢ 𝒫 𝑡 ∈ V
7 6 inex2 ⊢ ( 𝐽 ∩ 𝒫 𝑡 ) ∈ V
8 7 uniex ⊢ ∪ ( 𝐽 ∩ 𝒫 𝑡 ) ∈ V
9 8 rgenw ⊢ ∀ 𝑡 ∈ 𝒫 𝑋 ∪ ( 𝐽 ∩ 𝒫 𝑡 ) ∈ V
10 nfcv ⊢ Ⅎ 𝑡 𝒫 𝑋
11 10 fnmptf ⊢ ( ∀ 𝑡 ∈ 𝒫 𝑋 ∪ ( 𝐽 ∩ 𝒫 𝑡 ) ∈ V → ( 𝑡 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑡 ) ) Fn 𝒫 𝑋 )
12 9 11 mp1i ⊢ ( 𝐽 ∈ Top → ( 𝑡 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑡 ) ) Fn 𝒫 𝑋 )
13 1 ntrfval ⊢ ( 𝐽 ∈ Top → ( int ‘ 𝐽 ) = ( 𝑡 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑡 ) ) )
14 3 13 syl5eq ⊢ ( 𝐽 ∈ Top → 𝐼 = ( 𝑡 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑡 ) ) )
15 14 fneq1d ⊢ ( 𝐽 ∈ Top → ( 𝐼 Fn 𝒫 𝑋 ↔ ( 𝑡 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑡 ) ) Fn 𝒫 𝑋 ) )
16 12 15 mpbird ⊢ ( 𝐽 ∈ Top → 𝐼 Fn 𝒫 𝑋 )
17 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
18 4 5 17 dssmapf1od ⊢ ( 𝐽 ∈ Top → 𝐷 : ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) –1-1-onto→ ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) )
19 f1of ⊢ ( 𝐷 : ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) –1-1-onto→ ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) → 𝐷 : ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) ⟶ ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) )
20 18 19 syl ⊢ ( 𝐽 ∈ Top → 𝐷 : ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) ⟶ ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) )
21 1 2 clselmap ⊢ ( 𝐽 ∈ Top → 𝐾 ∈ ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) )
22 20 21 ffvelrnd ⊢ ( 𝐽 ∈ Top → ( 𝐷 ‘ 𝐾 ) ∈ ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) )
23 elmapfn ⊢ ( ( 𝐷 ‘ 𝐾 ) ∈ ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) → ( 𝐷 ‘ 𝐾 ) Fn 𝒫 𝑋 )
24 22 23 syl ⊢ ( 𝐽 ∈ Top → ( 𝐷 ‘ 𝐾 ) Fn 𝒫 𝑋 )
25 elpwi ⊢ ( 𝑡 ∈ 𝒫 𝑋 → 𝑡 ⊆ 𝑋 )
26 1 ntrval2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑡 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑡 ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑡 ) ) ) )
27 25 26 sylan2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑡 ∈ 𝒫 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑡 ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑡 ) ) ) )
28 3 fveq1i ⊢ ( 𝐼 ‘ 𝑡 ) = ( ( int ‘ 𝐽 ) ‘ 𝑡 )
29 2 fveq1i ⊢ ( 𝐾 ‘ ( 𝑋 ∖ 𝑡 ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑡 ) )
30 29 difeq2i ⊢ ( 𝑋 ∖ ( 𝐾 ‘ ( 𝑋 ∖ 𝑡 ) ) ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑡 ) ) )
31 27 28 30 3eqtr4g ⊢ ( ( 𝐽 ∈ Top ∧ 𝑡 ∈ 𝒫 𝑋 ) → ( 𝐼 ‘ 𝑡 ) = ( 𝑋 ∖ ( 𝐾 ‘ ( 𝑋 ∖ 𝑡 ) ) ) )
32 17 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑡 ∈ 𝒫 𝑋 ) → 𝑋 ∈ 𝐽 )
33 21 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑡 ∈ 𝒫 𝑋 ) → 𝐾 ∈ ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) )
34 eqid ⊢ ( 𝐷 ‘ 𝐾 ) = ( 𝐷 ‘ 𝐾 )
35 simpr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑡 ∈ 𝒫 𝑋 ) → 𝑡 ∈ 𝒫 𝑋 )
36 eqid ⊢ ( ( 𝐷 ‘ 𝐾 ) ‘ 𝑡 ) = ( ( 𝐷 ‘ 𝐾 ) ‘ 𝑡 )
37 4 5 32 33 34 35 36 dssmapfv3d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑡 ∈ 𝒫 𝑋 ) → ( ( 𝐷 ‘ 𝐾 ) ‘ 𝑡 ) = ( 𝑋 ∖ ( 𝐾 ‘ ( 𝑋 ∖ 𝑡 ) ) ) )
38 31 37 eqtr4d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑡 ∈ 𝒫 𝑋 ) → ( 𝐼 ‘ 𝑡 ) = ( ( 𝐷 ‘ 𝐾 ) ‘ 𝑡 ) )
39 16 24 38 eqfnfvd ⊢ ( 𝐽 ∈ Top → 𝐼 = ( 𝐷 ‘ 𝐾 ) )