Metamath Proof Explorer


Theorem cnclsi

Description: Property of the image of a closure. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis cnclsi.1 X = J
Assertion cnclsi F J Cn K S X F cls J S cls K F S

Proof

Step Hyp Ref Expression
1 cnclsi.1 X = J
2 cntop1 F J Cn K J Top
3 2 adantr F J Cn K S X J Top
4 cnvimass F -1 F S dom F
5 eqid K = K
6 1 5 cnf F J Cn K F : X K
7 6 adantr F J Cn K S X F : X K
8 4 7 fssdm F J Cn K S X F -1 F S X
9 simpr F J Cn K S X S X
10 7 fdmd F J Cn K S X dom F = X
11 9 10 sseqtrrd F J Cn K S X S dom F
12 sseqin2 S dom F dom F S = S
13 11 12 sylib F J Cn K S X dom F S = S
14 dminss dom F S F -1 F S
15 13 14 eqsstrrdi F J Cn K S X S F -1 F S
16 1 clsss J Top F -1 F S X S F -1 F S cls J S cls J F -1 F S
17 3 8 15 16 syl3anc F J Cn K S X cls J S cls J F -1 F S
18 imassrn F S ran F
19 7 frnd F J Cn K S X ran F K
20 18 19 sstrid F J Cn K S X F S K
21 5 cncls2i F J Cn K F S K cls J F -1 F S F -1 cls K F S
22 20 21 syldan F J Cn K S X cls J F -1 F S F -1 cls K F S
23 17 22 sstrd F J Cn K S X cls J S F -1 cls K F S
24 7 ffund F J Cn K S X Fun F
25 1 clsss3 J Top S X cls J S X
26 2 25 sylan F J Cn K S X cls J S X
27 26 10 sseqtrrd F J Cn K S X cls J S dom F
28 funimass3 Fun F cls J S dom F F cls J S cls K F S cls J S F -1 cls K F S
29 24 27 28 syl2anc F J Cn K S X F cls J S cls K F S cls J S F -1 cls K F S
30 23 29 mpbird F J Cn K S X F cls J S cls K F S