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	eqtrid	⊢ ( 𝐽 ∈ 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	ffvelcdmd	⊢ ( 𝐽 ∈ 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 → 𝐼 = ( 𝐷 ‘ 𝐾 ) )