Metamath Proof Explorer

Theorem ntrclsss

Description: If interior and closure functions are related then a subset relation of a pair of function values is equivalent to subset relation 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 ntrclsss ( 𝜑 → ( ( 𝐼 ‘ 𝑆 ) ⊆ ( 𝐼 ‘ 𝑇 ) ↔ ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ⊆ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ) )

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 4 ntrclsfv ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑆 ) = ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ) )
7 1 2 3 5 ntrclsfv ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑇 ) = ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ) )
8 6 7 sseq12d ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑆 ) ⊆ ( 𝐼 ‘ 𝑇 ) ↔ ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ) ⊆ ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ) ) )
9 1 2 3 ntrclskex ⊢ ( 𝜑 → 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
10 9 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) )
11 elmapi ⊢ ( 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐾 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
12 11 adantl ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → 𝐾 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
13 2 3 ntrclsrcomplex ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑇 ) ∈ 𝒫 𝐵 )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( 𝐵 ∖ 𝑇 ) ∈ 𝒫 𝐵 )
15 12 14 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ∈ 𝒫 𝐵 )
16 15 elpwid ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ⊆ 𝐵 )
17 2 3 ntrclsrcomplex ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑆 ) ∈ 𝒫 𝐵 )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( 𝐵 ∖ 𝑆 ) ∈ 𝒫 𝐵 )
19 12 18 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ∈ 𝒫 𝐵 )
20 19 elpwid ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ⊆ 𝐵 )
21 16 20 jca ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ⊆ 𝐵 ∧ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ⊆ 𝐵 ) )
22 sscon34b ⊢ ( ( ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ⊆ 𝐵 ∧ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ⊆ 𝐵 ) → ( ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ⊆ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ↔ ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ) ⊆ ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ) ) )
23 10 21 22 3syl ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ⊆ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ↔ ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ) ⊆ ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ) ) )
24 8 23 bitr4d ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑆 ) ⊆ ( 𝐼 ‘ 𝑇 ) ↔ ( 𝐾 ‘ ( 𝐵 ∖ 𝑇 ) ) ⊆ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ) )