Theorem ntrclsfv1

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then there is a functional relation between them (Contributed by RP, 28-May-2021)

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

Proof

Step	Hyp	Ref	Expression
1		ntrcls.o	⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
2		ntrcls.d	⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
3		ntrcls.r	⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
4	1 2 3	ntrclsf1o	⊢ ( 𝜑 → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
5		f1ofn	⊢ ( 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐷 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
6	4 5	syl	⊢ ( 𝜑 → 𝐷 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
7	1 2 3	ntrclsiex	⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
8	6 7	jca	⊢ ( 𝜑 → ( 𝐷 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) )
9		fnfun	⊢ ( 𝐷 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → Fun 𝐷 )
10	9	adantr	⊢ ( ( 𝐷 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → Fun 𝐷 )
11		fndm	⊢ ( 𝐷 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → dom 𝐷 = ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
12	11	eleq2d	⊢ ( 𝐷 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → ( 𝐼 ∈ dom 𝐷 ↔ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) )
13	12	biimpar	⊢ ( ( 𝐷 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → 𝐼 ∈ dom 𝐷 )
14	10 13	jca	⊢ ( ( 𝐷 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( Fun 𝐷 ∧ 𝐼 ∈ dom 𝐷 ) )
15	8 14	syl	⊢ ( 𝜑 → ( Fun 𝐷 ∧ 𝐼 ∈ dom 𝐷 ) )
16		funbrfvb	⊢ ( ( Fun 𝐷 ∧ 𝐼 ∈ dom 𝐷 ) → ( ( 𝐷 ‘ 𝐼 ) = 𝐾 ↔ 𝐼 𝐷 𝐾 ) )
17	15 16	syl	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐼 ) = 𝐾 ↔ 𝐼 𝐷 𝐾 ) )
18	3 17	mpbird	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐼 ) = 𝐾 )