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 
|- O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) )
ntrcls.d 
|- D = ( O ` B )
ntrcls.r 
|- ( ph -> I D K )
ntrclsfv.s 
|- ( ph -> S e. ~P B )
ntrclsfv.t 
|- ( ph -> T e. ~P B )
Assertion ntrclsss 
|- ( ph -> ( ( I ` S ) C_ ( I ` T ) <-> ( K ` ( B \ T ) ) C_ ( K ` ( B \ S ) ) ) )

Proof

Step Hyp Ref Expression
1 ntrcls.o 
 |-  O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) )
2 ntrcls.d 
 |-  D = ( O ` B )
3 ntrcls.r 
 |-  ( ph -> I D K )
4 ntrclsfv.s 
 |-  ( ph -> S e. ~P B )
5 ntrclsfv.t 
 |-  ( ph -> T e. ~P B )
6 1 2 3 4 ntrclsfv 
 |-  ( ph -> ( I ` S ) = ( B \ ( K ` ( B \ S ) ) ) )
7 1 2 3 5 ntrclsfv 
 |-  ( ph -> ( I ` T ) = ( B \ ( K ` ( B \ T ) ) ) )
8 6 7 sseq12d 
 |-  ( ph -> ( ( I ` S ) C_ ( I ` T ) <-> ( B \ ( K ` ( B \ S ) ) ) C_ ( B \ ( K ` ( B \ T ) ) ) ) )
9 1 2 3 ntrclskex 
 |-  ( ph -> K e. ( ~P B ^m ~P B ) )
10 9 ancli 
 |-  ( ph -> ( ph /\ K e. ( ~P B ^m ~P B ) ) )
11 elmapi 
 |-  ( K e. ( ~P B ^m ~P B ) -> K : ~P B --> ~P B )
12 11 adantl 
 |-  ( ( ph /\ K e. ( ~P B ^m ~P B ) ) -> K : ~P B --> ~P B )
13 2 3 ntrclsrcomplex 
 |-  ( ph -> ( B \ T ) e. ~P B )
14 13 adantr 
 |-  ( ( ph /\ K e. ( ~P B ^m ~P B ) ) -> ( B \ T ) e. ~P B )
15 12 14 ffvelrnd 
 |-  ( ( ph /\ K e. ( ~P B ^m ~P B ) ) -> ( K ` ( B \ T ) ) e. ~P B )
16 15 elpwid 
 |-  ( ( ph /\ K e. ( ~P B ^m ~P B ) ) -> ( K ` ( B \ T ) ) C_ B )
17 2 3 ntrclsrcomplex 
 |-  ( ph -> ( B \ S ) e. ~P B )
18 17 adantr 
 |-  ( ( ph /\ K e. ( ~P B ^m ~P B ) ) -> ( B \ S ) e. ~P B )
19 12 18 ffvelrnd 
 |-  ( ( ph /\ K e. ( ~P B ^m ~P B ) ) -> ( K ` ( B \ S ) ) e. ~P B )
20 19 elpwid 
 |-  ( ( ph /\ K e. ( ~P B ^m ~P B ) ) -> ( K ` ( B \ S ) ) C_ B )
21 16 20 jca 
 |-  ( ( ph /\ K e. ( ~P B ^m ~P B ) ) -> ( ( K ` ( B \ T ) ) C_ B /\ ( K ` ( B \ S ) ) C_ B ) )
22 sscon34b 
 |-  ( ( ( K ` ( B \ T ) ) C_ B /\ ( K ` ( B \ S ) ) C_ B ) -> ( ( K ` ( B \ T ) ) C_ ( K ` ( B \ S ) ) <-> ( B \ ( K ` ( B \ S ) ) ) C_ ( B \ ( K ` ( B \ T ) ) ) ) )
23 10 21 22 3syl 
 |-  ( ph -> ( ( K ` ( B \ T ) ) C_ ( K ` ( B \ S ) ) <-> ( B \ ( K ` ( B \ S ) ) ) C_ ( B \ ( K ` ( B \ T ) ) ) ) )
24 8 23 bitr4d 
 |-  ( ph -> ( ( I ` S ) C_ ( I ` T ) <-> ( K ` ( B \ T ) ) C_ ( K ` ( B \ S ) ) ) )