This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnntri

Description: Property of the preimage of an interior. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis cncls2i.1 
|- Y = U. K
Assertion cnntri 
|- ( ( F e. ( J Cn K ) /\ S C_ Y ) -> ( `' F " ( ( int ` K ) ` S ) ) C_ ( ( int ` J ) ` ( `' F " S ) ) )

Proof

Step Hyp Ref Expression
1 cncls2i.1 
 |-  Y = U. K
2 cntop1 
 |-  ( F e. ( J Cn K ) -> J e. Top )
3 2 adantr 
 |-  ( ( F e. ( J Cn K ) /\ S C_ Y ) -> J e. Top )
4 cnvimass 
 |-  ( `' F " S ) C_ dom F
5 eqid 
 |-  U. J = U. J
6 5 1 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> Y )
7 6 fdmd 
 |-  ( F e. ( J Cn K ) -> dom F = U. J )
8 7 adantr 
 |-  ( ( F e. ( J Cn K ) /\ S C_ Y ) -> dom F = U. J )
9 4 8 sseqtrid 
 |-  ( ( F e. ( J Cn K ) /\ S C_ Y ) -> ( `' F " S ) C_ U. J )
10 cntop2 
 |-  ( F e. ( J Cn K ) -> K e. Top )
11 1 ntropn 
 |-  ( ( K e. Top /\ S C_ Y ) -> ( ( int ` K ) ` S ) e. K )
12 10 11 sylan 
 |-  ( ( F e. ( J Cn K ) /\ S C_ Y ) -> ( ( int ` K ) ` S ) e. K )
13 cnima 
 |-  ( ( F e. ( J Cn K ) /\ ( ( int ` K ) ` S ) e. K ) -> ( `' F " ( ( int ` K ) ` S ) ) e. J )
14 12 13 syldan 
 |-  ( ( F e. ( J Cn K ) /\ S C_ Y ) -> ( `' F " ( ( int ` K ) ` S ) ) e. J )
15 1 ntrss2 
 |-  ( ( K e. Top /\ S C_ Y ) -> ( ( int ` K ) ` S ) C_ S )
16 10 15 sylan 
 |-  ( ( F e. ( J Cn K ) /\ S C_ Y ) -> ( ( int ` K ) ` S ) C_ S )
17 imass2 
 |-  ( ( ( int ` K ) ` S ) C_ S -> ( `' F " ( ( int ` K ) ` S ) ) C_ ( `' F " S ) )
18 16 17 syl 
 |-  ( ( F e. ( J Cn K ) /\ S C_ Y ) -> ( `' F " ( ( int ` K ) ` S ) ) C_ ( `' F " S ) )
19 5 ssntr 
 |-  ( ( ( J e. Top /\ ( `' F " S ) C_ U. J ) /\ ( ( `' F " ( ( int ` K ) ` S ) ) e. J /\ ( `' F " ( ( int ` K ) ` S ) ) C_ ( `' F " S ) ) ) -> ( `' F " ( ( int ` K ) ` S ) ) C_ ( ( int ` J ) ` ( `' F " S ) ) )
20 3 9 14 18 19 syl22anc 
 |-  ( ( F e. ( J Cn K ) /\ S C_ Y ) -> ( `' F " ( ( int ` K ) ` S ) ) C_ ( ( int ` J ) ` ( `' F " S ) ) )