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 JTopOnXKTopOnYFJCnKF:XYx𝒫XFclsJxclsKFx

Proof

Step Hyp Ref Expression
1 cnf2 JTopOnXKTopOnYFJCnKF:XY
2 1 3expia JTopOnXKTopOnYFJCnKF:XY
3 elpwi x𝒫XxX
4 3 adantl JTopOnXKTopOnYx𝒫XxX
5 toponuni JTopOnXX=J
6 5 ad2antrr JTopOnXKTopOnYx𝒫XX=J
7 4 6 sseqtrd JTopOnXKTopOnYx𝒫XxJ
8 eqid J=J
9 8 cnclsi FJCnKxJFclsJxclsKFx
10 9 expcom xJFJCnKFclsJxclsKFx
11 7 10 syl JTopOnXKTopOnYx𝒫XFJCnKFclsJxclsKFx
12 11 ralrimdva JTopOnXKTopOnYFJCnKx𝒫XFclsJxclsKFx
13 2 12 jcad JTopOnXKTopOnYFJCnKF:XYx𝒫XFclsJxclsKFx
14 toponmax JTopOnXXJ
15 14 ad3antrrr JTopOnXKTopOnYF:XYy𝒫YXJ
16 cnvimass F-1ydomF
17 fdm F:XYdomF=X
18 17 ad2antlr JTopOnXKTopOnYF:XYy𝒫YdomF=X
19 16 18 sseqtrid JTopOnXKTopOnYF:XYy𝒫YF-1yX
20 15 19 sselpwd JTopOnXKTopOnYF:XYy𝒫YF-1y𝒫X
21 fveq2 x=F-1yclsJx=clsJF-1y
22 21 imaeq2d x=F-1yFclsJx=FclsJF-1y
23 imaeq2 x=F-1yFx=FF-1y
24 23 fveq2d x=F-1yclsKFx=clsKFF-1y
25 22 24 sseq12d x=F-1yFclsJxclsKFxFclsJF-1yclsKFF-1y
26 25 rspcv F-1y𝒫Xx𝒫XFclsJxclsKFxFclsJF-1yclsKFF-1y
27 20 26 syl JTopOnXKTopOnYF:XYy𝒫Yx𝒫XFclsJxclsKFxFclsJF-1yclsKFF-1y
28 topontop KTopOnYKTop
29 28 ad3antlr JTopOnXKTopOnYF:XYy𝒫YKTop
30 elpwi y𝒫YyY
31 30 adantl JTopOnXKTopOnYF:XYy𝒫YyY
32 toponuni KTopOnYY=K
33 32 ad3antlr JTopOnXKTopOnYF:XYy𝒫YY=K
34 31 33 sseqtrd JTopOnXKTopOnYF:XYy𝒫YyK
35 ffun F:XYFunF
36 35 ad2antlr JTopOnXKTopOnYF:XYy𝒫YFunF
37 funimacnv FunFFF-1y=yranF
38 36 37 syl JTopOnXKTopOnYF:XYy𝒫YFF-1y=yranF
39 inss1 yranFy
40 38 39 eqsstrdi JTopOnXKTopOnYF:XYy𝒫YFF-1yy
41 eqid K=K
42 41 clsss KTopyKFF-1yyclsKFF-1yclsKy
43 29 34 40 42 syl3anc JTopOnXKTopOnYF:XYy𝒫YclsKFF-1yclsKy
44 sstr2 FclsJF-1yclsKFF-1yclsKFF-1yclsKyFclsJF-1yclsKy
45 43 44 syl5com JTopOnXKTopOnYF:XYy𝒫YFclsJF-1yclsKFF-1yFclsJF-1yclsKy
46 topontop JTopOnXJTop
47 46 ad3antrrr JTopOnXKTopOnYF:XYy𝒫YJTop
48 5 ad3antrrr JTopOnXKTopOnYF:XYy𝒫YX=J
49 18 48 eqtrd JTopOnXKTopOnYF:XYy𝒫YdomF=J
50 16 49 sseqtrid JTopOnXKTopOnYF:XYy𝒫YF-1yJ
51 8 clsss3 JTopF-1yJclsJF-1yJ
52 47 50 51 syl2anc JTopOnXKTopOnYF:XYy𝒫YclsJF-1yJ
53 52 49 sseqtrrd JTopOnXKTopOnYF:XYy𝒫YclsJF-1ydomF
54 funimass3 FunFclsJF-1ydomFFclsJF-1yclsKyclsJF-1yF-1clsKy
55 36 53 54 syl2anc JTopOnXKTopOnYF:XYy𝒫YFclsJF-1yclsKyclsJF-1yF-1clsKy
56 45 55 sylibd JTopOnXKTopOnYF:XYy𝒫YFclsJF-1yclsKFF-1yclsJF-1yF-1clsKy
57 27 56 syld JTopOnXKTopOnYF:XYy𝒫Yx𝒫XFclsJxclsKFxclsJF-1yF-1clsKy
58 57 ralrimdva JTopOnXKTopOnYF:XYx𝒫XFclsJxclsKFxy𝒫YclsJF-1yF-1clsKy
59 58 imdistanda JTopOnXKTopOnYF:XYx𝒫XFclsJxclsKFxF:XYy𝒫YclsJF-1yF-1clsKy
60 cncls2 JTopOnXKTopOnYFJCnKF:XYy𝒫YclsJF-1yF-1clsKy
61 59 60 sylibrd JTopOnXKTopOnYF:XYx𝒫XFclsJxclsKFxFJCnK
62 13 61 impbid JTopOnXKTopOnYFJCnKF:XYx𝒫XFclsJxclsKFx