Metamath Proof Explorer


Theorem cncls

Description: Continuity in terms of closure. (Contributed by Jeff Hankins, 1-Oct-2009) (Proof shortened by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion cncls J TopOn X K TopOn Y F J Cn K F : X Y x 𝒫 X F cls J x cls K F x

Proof

Step Hyp Ref Expression
1 cnf2 J TopOn X K TopOn Y F J Cn K F : X Y
2 1 3expia J TopOn X K TopOn Y F J Cn K F : X Y
3 elpwi x 𝒫 X x X
4 3 adantl J TopOn X K TopOn Y x 𝒫 X x X
5 toponuni J TopOn X X = J
6 5 ad2antrr J TopOn X K TopOn Y x 𝒫 X X = J
7 4 6 sseqtrd J TopOn X K TopOn Y x 𝒫 X x J
8 eqid J = J
9 8 cnclsi F J Cn K x J F cls J x cls K F x
10 9 expcom x J F J Cn K F cls J x cls K F x
11 7 10 syl J TopOn X K TopOn Y x 𝒫 X F J Cn K F cls J x cls K F x
12 11 ralrimdva J TopOn X K TopOn Y F J Cn K x 𝒫 X F cls J x cls K F x
13 2 12 jcad J TopOn X K TopOn Y F J Cn K F : X Y x 𝒫 X F cls J x cls K F x
14 toponmax J TopOn X X J
15 14 ad3antrrr J TopOn X K TopOn Y F : X Y y 𝒫 Y X J
16 cnvimass F -1 y dom F
17 fdm F : X Y dom F = X
18 17 ad2antlr J TopOn X K TopOn Y F : X Y y 𝒫 Y dom F = X
19 16 18 sseqtrid J TopOn X K TopOn Y F : X Y y 𝒫 Y F -1 y X
20 15 19 sselpwd J TopOn X K TopOn Y F : X Y y 𝒫 Y F -1 y 𝒫 X
21 fveq2 x = F -1 y cls J x = cls J F -1 y
22 21 imaeq2d x = F -1 y F cls J x = F cls J F -1 y
23 imaeq2 x = F -1 y F x = F F -1 y
24 23 fveq2d x = F -1 y cls K F x = cls K F F -1 y
25 22 24 sseq12d x = F -1 y F cls J x cls K F x F cls J F -1 y cls K F F -1 y
26 25 rspcv F -1 y 𝒫 X x 𝒫 X F cls J x cls K F x F cls J F -1 y cls K F F -1 y
27 20 26 syl J TopOn X K TopOn Y F : X Y y 𝒫 Y x 𝒫 X F cls J x cls K F x F cls J F -1 y cls K F F -1 y
28 topontop K TopOn Y K Top
29 28 ad3antlr J TopOn X K TopOn Y F : X Y y 𝒫 Y K Top
30 elpwi y 𝒫 Y y Y
31 30 adantl J TopOn X K TopOn Y F : X Y y 𝒫 Y y Y
32 toponuni K TopOn Y Y = K
33 32 ad3antlr J TopOn X K TopOn Y F : X Y y 𝒫 Y Y = K
34 31 33 sseqtrd J TopOn X K TopOn Y F : X Y y 𝒫 Y y K
35 ffun F : X Y Fun F
36 35 ad2antlr J TopOn X K TopOn Y F : X Y y 𝒫 Y Fun F
37 funimacnv Fun F F F -1 y = y ran F
38 36 37 syl J TopOn X K TopOn Y F : X Y y 𝒫 Y F F -1 y = y ran F
39 inss1 y ran F y
40 38 39 eqsstrdi J TopOn X K TopOn Y F : X Y y 𝒫 Y F F -1 y y
41 eqid K = K
42 41 clsss K Top y K F F -1 y y cls K F F -1 y cls K y
43 29 34 40 42 syl3anc J TopOn X K TopOn Y F : X Y y 𝒫 Y cls K F F -1 y cls K y
44 sstr2 F cls J F -1 y cls K F F -1 y cls K F F -1 y cls K y F cls J F -1 y cls K y
45 43 44 syl5com J TopOn X K TopOn Y F : X Y y 𝒫 Y F cls J F -1 y cls K F F -1 y F cls J F -1 y cls K y
46 topontop J TopOn X J Top
47 46 ad3antrrr J TopOn X K TopOn Y F : X Y y 𝒫 Y J Top
48 5 ad3antrrr J TopOn X K TopOn Y F : X Y y 𝒫 Y X = J
49 18 48 eqtrd J TopOn X K TopOn Y F : X Y y 𝒫 Y dom F = J
50 16 49 sseqtrid J TopOn X K TopOn Y F : X Y y 𝒫 Y F -1 y J
51 8 clsss3 J Top F -1 y J cls J F -1 y J
52 47 50 51 syl2anc J TopOn X K TopOn Y F : X Y y 𝒫 Y cls J F -1 y J
53 52 49 sseqtrrd J TopOn X K TopOn Y F : X Y y 𝒫 Y cls J F -1 y dom F
54 funimass3 Fun F cls J F -1 y dom F F cls J F -1 y cls K y cls J F -1 y F -1 cls K y
55 36 53 54 syl2anc J TopOn X K TopOn Y F : X Y y 𝒫 Y F cls J F -1 y cls K y cls J F -1 y F -1 cls K y
56 45 55 sylibd J TopOn X K TopOn Y F : X Y y 𝒫 Y F cls J F -1 y cls K F F -1 y cls J F -1 y F -1 cls K y
57 27 56 syld J TopOn X K TopOn Y F : X Y y 𝒫 Y x 𝒫 X F cls J x cls K F x cls J F -1 y F -1 cls K y
58 57 ralrimdva J TopOn X K TopOn Y F : X Y x 𝒫 X F cls J x cls K F x y 𝒫 Y cls J F -1 y F -1 cls K y
59 58 imdistanda J TopOn X K TopOn Y F : X Y x 𝒫 X F cls J x cls K F x F : X Y y 𝒫 Y cls J F -1 y F -1 cls K y
60 cncls2 J TopOn X K TopOn Y F J Cn K F : X Y y 𝒫 Y cls J F -1 y F -1 cls K y
61 59 60 sylibrd J TopOn X K TopOn Y F : X Y x 𝒫 X F cls J x cls K F x F J Cn K
62 13 61 impbid J TopOn X K TopOn Y F J Cn K F : X Y x 𝒫 X F cls J x cls K F x