Theorem ntrclsfveq

Description: If interior and closure functions are related then equality of a pair of function values is equivalent to equality of a pair of the other function's values. (Contributed by RP, 27-Jun-2021)

	Ref	Expression
Hypotheses	ntrcls.o	⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
	ntrcls.d	⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
	ntrcls.r	⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
	ntrclsfv.s	⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
	ntrclsfv.t	⊢ ( 𝜑 → 𝑇 ∈ 𝒫 𝐵 )
Assertion	ntrclsfveq	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑆 ) = ( 𝐼 ‘ 𝑇 ) ↔ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) = ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ntrcls.o	⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
2		ntrcls.d	⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
3		ntrcls.r	⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
4		ntrclsfv.s	⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
5		ntrclsfv.t	⊢ ( 𝜑 → 𝑇 ∈ 𝒫 𝐵 )
6	1 2 3 5	ntrclsfv	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑇 ) = ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ) )
7	6	eqeq2d	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑆 ) = ( 𝐼 ‘ 𝑇 ) ↔ ( 𝐼 ‘ 𝑆 ) = ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ) ) )
8	2 3	ntrclsrcomplex	⊢ ( 𝜑 → ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ) ∈ 𝒫 𝐵 )
9	1 2 3 4 8	ntrclsfveq1	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑆 ) = ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ) ↔ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) = ( 𝐵 ∖ ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ) ) ) )
10	1 2 3	ntrclskex	⊢ ( 𝜑 → 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
11		elmapi	⊢ ( 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐾 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
12	10 11	syl	⊢ ( 𝜑 → 𝐾 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
13	2 3	ntrclsrcomplex	⊢ ( 𝜑 → ( 𝐵 ∖ 𝑇 ) ∈ 𝒫 𝐵 )
14	12 13	ffvelrnd	⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ∈ 𝒫 𝐵 )
15	14	elpwid	⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ⊆ 𝐵 )
16		dfss4	⊢ ( ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ⊆ 𝐵 ↔ ( 𝐵 ∖ ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ) ) = ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) )
17	15 16	sylib	⊢ ( 𝜑 → ( 𝐵 ∖ ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ) ) = ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) )
18	17	eqeq2d	⊢ ( 𝜑 → ( ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) = ( 𝐵 ∖ ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ) ) ↔ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) = ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ) )
19	7 9 18	3bitrd	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑆 ) = ( 𝐼 ‘ 𝑇 ) ↔ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) = ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ) )