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 ) ) )