Metamath Proof Explorer

Theorem ntrk2imkb

Description: If an interior function is contracting, the interiors of disjoint sets are disjoint. Kuratowski's K2 axiom implies KB. Interior version. (Contributed by RP, 9-Jun-2021)

Ref Expression
Assertion ntrk2imkb
`|- ( A. s e. ~P B ( I ` s ) C_ s -> A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) )`

Proof

Step Hyp Ref Expression
1 id
` |-  ( A. s e. ~P B ( I ` s ) C_ s -> A. s e. ~P B ( I ` s ) C_ s )`
2 fveq2
` |-  ( s = t -> ( I ` s ) = ( I ` t ) )`
3 id
` |-  ( s = t -> s = t )`
4 2 3 sseq12d
` |-  ( s = t -> ( ( I ` s ) C_ s <-> ( I ` t ) C_ t ) )`
5 4 cbvralvw
` |-  ( A. s e. ~P B ( I ` s ) C_ s <-> A. t e. ~P B ( I ` t ) C_ t )`
6 5 biimpi
` |-  ( A. s e. ~P B ( I ` s ) C_ s -> A. t e. ~P B ( I ` t ) C_ t )`
7 raaanv
` |-  ( A. s e. ~P B A. t e. ~P B ( ( I ` s ) C_ s /\ ( I ` t ) C_ t ) <-> ( A. s e. ~P B ( I ` s ) C_ s /\ A. t e. ~P B ( I ` t ) C_ t ) )`
8 1 6 7 sylanbrc
` |-  ( A. s e. ~P B ( I ` s ) C_ s -> A. s e. ~P B A. t e. ~P B ( ( I ` s ) C_ s /\ ( I ` t ) C_ t ) )`
9 ss2in
` |-  ( ( ( I ` s ) C_ s /\ ( I ` t ) C_ t ) -> ( ( I ` s ) i^i ( I ` t ) ) C_ ( s i^i t ) )`
10 9 adantr
` |-  ( ( ( ( I ` s ) C_ s /\ ( I ` t ) C_ t ) /\ ( s i^i t ) = (/) ) -> ( ( I ` s ) i^i ( I ` t ) ) C_ ( s i^i t ) )`
11 simpr
` |-  ( ( ( ( I ` s ) C_ s /\ ( I ` t ) C_ t ) /\ ( s i^i t ) = (/) ) -> ( s i^i t ) = (/) )`
12 10 11 sseqtrd
` |-  ( ( ( ( I ` s ) C_ s /\ ( I ` t ) C_ t ) /\ ( s i^i t ) = (/) ) -> ( ( I ` s ) i^i ( I ` t ) ) C_ (/) )`
13 ss0
` |-  ( ( ( I ` s ) i^i ( I ` t ) ) C_ (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) )`
14 12 13 syl
` |-  ( ( ( ( I ` s ) C_ s /\ ( I ` t ) C_ t ) /\ ( s i^i t ) = (/) ) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) )`
15 14 ex
` |-  ( ( ( I ` s ) C_ s /\ ( I ` t ) C_ t ) -> ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) )`
16 15 2ralimi
` |-  ( A. s e. ~P B A. t e. ~P B ( ( I ` s ) C_ s /\ ( I ` t ) C_ t ) -> A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) )`
17 8 16 syl
` |-  ( A. s e. ~P B ( I ` s ) C_ s -> A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) )`