Theorem dssmapclsntr

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

	Ref	Expression
Hypotheses	dssmapclsntr.x	⊢ 𝑋 = ∪ 𝐽
	dssmapclsntr.k	⊢ 𝐾 = ( cls ‘ 𝐽 )
	dssmapclsntr.i	⊢ 𝐼 = ( int ‘ 𝐽 )
	dssmapclsntr.o	⊢ 𝑂 = ( 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝒫 𝑏 ) ↦ ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) ) ) ) )
	dssmapclsntr.d	⊢ 𝐷 = ( 𝑂 ‘ 𝑋 )
Assertion	dssmapclsntr	⊢ ( 𝐽 ∈ 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	1 2 3 4 5	dssmapntrcls	⊢ ( 𝐽 ∈ Top → 𝐼 = ( 𝐷 ‘ 𝐾 ) )
7	6	eqcomd	⊢ ( 𝐽 ∈ Top → ( 𝐷 ‘ 𝐾 ) = 𝐼 )
8	1	topopn	⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
9	4 5 8	dssmapf1od	⊢ ( 𝐽 ∈ Top → 𝐷 : ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) –1-1-onto→ ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) )
10	1 2	clselmap	⊢ ( 𝐽 ∈ Top → 𝐾 ∈ ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) )
11		f1ocnvfv	⊢ ( ( 𝐷 : ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) –1-1-onto→ ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) ∧ 𝐾 ∈ ( 𝒫 𝑋 ↑m 𝒫 𝑋 ) ) → ( ( 𝐷 ‘ 𝐾 ) = 𝐼 → ( ◡ 𝐷 ‘ 𝐼 ) = 𝐾 ) )
12	9 10 11	syl2anc	⊢ ( 𝐽 ∈ Top → ( ( 𝐷 ‘ 𝐾 ) = 𝐼 → ( ◡ 𝐷 ‘ 𝐼 ) = 𝐾 ) )
13	7 12	mpd	⊢ ( 𝐽 ∈ Top → ( ◡ 𝐷 ‘ 𝐼 ) = 𝐾 )
14	4 5 8	dssmapnvod	⊢ ( 𝐽 ∈ Top → ◡ 𝐷 = 𝐷 )
15	14	fveq1d	⊢ ( 𝐽 ∈ Top → ( ◡ 𝐷 ‘ 𝐼 ) = ( 𝐷 ‘ 𝐼 ) )
16	13 15	eqtr3d	⊢ ( 𝐽 ∈ Top → 𝐾 = ( 𝐷 ‘ 𝐼 ) )