# 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
`|- 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 ntrclsfveq
`|- ( ph -> ( ( I ` S ) = ( I ` T ) <-> ( K ` ( B \ S ) ) = ( K ` ( B \ T ) ) ) )`

### 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 5 ntrclsfv
` |-  ( ph -> ( I ` T ) = ( B \ ( K ` ( B \ T ) ) ) )`
7 6 eqeq2d
` |-  ( ph -> ( ( I ` S ) = ( I ` T ) <-> ( I ` S ) = ( B \ ( K ` ( B \ T ) ) ) ) )`
8 2 3 ntrclsrcomplex
` |-  ( ph -> ( B \ ( K ` ( B \ T ) ) ) e. ~P B )`
9 1 2 3 4 8 ntrclsfveq1
` |-  ( ph -> ( ( I ` S ) = ( B \ ( K ` ( B \ T ) ) ) <-> ( K ` ( B \ S ) ) = ( B \ ( B \ ( K ` ( B \ T ) ) ) ) ) )`
10 1 2 3 ntrclskex
` |-  ( ph -> K e. ( ~P B ^m ~P B ) )`
11 elmapi
` |-  ( K e. ( ~P B ^m ~P B ) -> K : ~P B --> ~P B )`
12 10 11 syl
` |-  ( ph -> K : ~P B --> ~P B )`
13 2 3 ntrclsrcomplex
` |-  ( ph -> ( B \ T ) e. ~P B )`
14 12 13 ffvelrnd
` |-  ( ph -> ( K ` ( B \ T ) ) e. ~P B )`
15 14 elpwid
` |-  ( ph -> ( K ` ( B \ T ) ) C_ B )`
16 dfss4
` |-  ( ( K ` ( B \ T ) ) C_ B <-> ( B \ ( B \ ( K ` ( B \ T ) ) ) ) = ( K ` ( B \ T ) ) )`
17 15 16 sylib
` |-  ( ph -> ( B \ ( B \ ( K ` ( B \ T ) ) ) ) = ( K ` ( B \ T ) ) )`
18 17 eqeq2d
` |-  ( ph -> ( ( K ` ( B \ S ) ) = ( B \ ( B \ ( K ` ( B \ T ) ) ) ) <-> ( K ` ( B \ S ) ) = ( K ` ( B \ T ) ) ) )`
19 7 9 18 3bitrd
` |-  ( ph -> ( ( I ` S ) = ( I ` T ) <-> ( K ` ( B \ S ) ) = ( K ` ( B \ T ) ) ) )`