# Metamath Proof Explorer

## 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 ( 𝜑 → ( ( 𝐼𝑆 ) = ( 𝐼𝑇 ) ↔ ( 𝐾 ‘ ( 𝐵𝑆 ) ) = ( 𝐾 ‘ ( 𝐵𝑇 ) ) ) )