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 = K
Assertion cnntri F J Cn K S Y F -1 int K S int J F -1 S

Proof

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