Theorem ntrclsnvobr

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then they are related the opposite way. (Contributed by RP, 21-May-2021)

	Ref	Expression
Hypotheses	ntrcls.o	⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
	ntrcls.d	⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
	ntrcls.r	⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
Assertion	ntrclsnvobr	⊢ ( 𝜑 → 𝐾 𝐷 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		ntrcls.o	⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
2		ntrcls.d	⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
3		ntrcls.r	⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
4	2 3	ntrclsbex	⊢ ( 𝜑 → 𝐵 ∈ V )
5	1 2 4	dssmapnvod	⊢ ( 𝜑 → ◡ 𝐷 = 𝐷 )
6	1 2 3	ntrclsf1o	⊢ ( 𝜑 → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
7		f1orel	⊢ ( 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → Rel 𝐷 )
8		relbrcnvg	⊢ ( Rel 𝐷 → ( 𝐾 ◡ 𝐷 𝐼 ↔ 𝐼 𝐷 𝐾 ) )
9	6 7 8	3syl	⊢ ( 𝜑 → ( 𝐾 ◡ 𝐷 𝐼 ↔ 𝐼 𝐷 𝐾 ) )
10	3 9	mpbird	⊢ ( 𝜑 → 𝐾 ◡ 𝐷 𝐼 )
11	5 10	breqdi	⊢ ( 𝜑 → 𝐾 𝐷 𝐼 )