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 ) ) = (/) ) )