Metamath Proof Explorer

Theorem ntrclsfveq1

Description: If interior and closure functions are related then specific function values are complementary. (Contributed by RP, 27-Jun-2021)

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

Proof

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