Metamath Proof Explorer


Theorem cncmp

Description: Compactness is respected by a continuous onto map. (Contributed by Jeff Hankins, 12-Jul-2009) (Proof shortened by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypothesis cncmp.2 Y=K
Assertion cncmp JCompF:XontoYFJCnKKComp

Proof

Step Hyp Ref Expression
1 cncmp.2 Y=K
2 cntop2 FJCnKKTop
3 2 3ad2ant3 JCompF:XontoYFJCnKKTop
4 elpwi u𝒫KuK
5 simpl1 JCompF:XontoYFJCnKuKY=uJComp
6 simpl3 JCompF:XontoYFJCnKuKY=uFJCnK
7 simprl JCompF:XontoYFJCnKuKY=uuK
8 7 sselda JCompF:XontoYFJCnKuKY=uyuyK
9 cnima FJCnKyKF-1yJ
10 6 8 9 syl2an2r JCompF:XontoYFJCnKuKY=uyuF-1yJ
11 10 fmpttd JCompF:XontoYFJCnKuKY=uyuF-1y:uJ
12 11 frnd JCompF:XontoYFJCnKuKY=uranyuF-1yJ
13 simprr JCompF:XontoYFJCnKuKY=uY=u
14 13 imaeq2d JCompF:XontoYFJCnKuKY=uF-1Y=F-1u
15 eqid J=J
16 15 1 cnf FJCnKF:JY
17 6 16 syl JCompF:XontoYFJCnKuKY=uF:JY
18 fimacnv F:JYF-1Y=J
19 17 18 syl JCompF:XontoYFJCnKuKY=uF-1Y=J
20 10 ralrimiva JCompF:XontoYFJCnKuKY=uyuF-1yJ
21 dfiun2g yuF-1yJyuF-1y=x|yux=F-1y
22 20 21 syl JCompF:XontoYFJCnKuKY=uyuF-1y=x|yux=F-1y
23 imauni F-1u=yuF-1y
24 eqid yuF-1y=yuF-1y
25 24 rnmpt ranyuF-1y=x|yux=F-1y
26 25 unieqi ranyuF-1y=x|yux=F-1y
27 22 23 26 3eqtr4g JCompF:XontoYFJCnKuKY=uF-1u=ranyuF-1y
28 14 19 27 3eqtr3d JCompF:XontoYFJCnKuKY=uJ=ranyuF-1y
29 15 cmpcov JCompranyuF-1yJJ=ranyuF-1ys𝒫ranyuF-1yFinJ=s
30 5 12 28 29 syl3anc JCompF:XontoYFJCnKuKY=us𝒫ranyuF-1yFinJ=s
31 elfpw s𝒫ranyuF-1yFinsranyuF-1ysFin
32 simprll JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=ssranyuF-1y
33 32 sselda JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=scscranyuF-1y
34 simpll2 JCompF:XontoYFJCnKuKY=uyuF:XontoY
35 elssuni yKyK
36 35 1 sseqtrrdi yKyY
37 8 36 syl JCompF:XontoYFJCnKuKY=uyuyY
38 foimacnv F:XontoYyYFF-1y=y
39 34 37 38 syl2anc JCompF:XontoYFJCnKuKY=uyuFF-1y=y
40 simpr JCompF:XontoYFJCnKuKY=uyuyu
41 39 40 eqeltrd JCompF:XontoYFJCnKuKY=uyuFF-1yu
42 41 ralrimiva JCompF:XontoYFJCnKuKY=uyuFF-1yu
43 imaeq2 c=F-1yFc=FF-1y
44 43 eleq1d c=F-1yFcuFF-1yu
45 24 44 ralrnmptw yuF-1yJcranyuF-1yFcuyuFF-1yu
46 20 45 syl JCompF:XontoYFJCnKuKY=ucranyuF-1yFcuyuFF-1yu
47 42 46 mpbird JCompF:XontoYFJCnKuKY=ucranyuF-1yFcu
48 47 adantr JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=scranyuF-1yFcu
49 48 r19.21bi JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=scranyuF-1yFcu
50 33 49 syldan JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=scsFcu
51 50 fmpttd JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=scsFc:su
52 51 frnd JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=srancsFcu
53 simprlr JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=ssFin
54 eqid csFc=csFc
55 54 rnmpt rancsFc=d|csd=Fc
56 abrexfi sFind|csd=FcFin
57 55 56 eqeltrid sFinrancsFcFin
58 53 57 syl JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=srancsFcFin
59 elfpw rancsFc𝒫uFinrancsFcurancsFcFin
60 52 58 59 sylanbrc JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=srancsFc𝒫uFin
61 17 adantr JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=sF:JY
62 61 fdmd JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=sdomF=J
63 simpll2 JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=sF:XontoY
64 fof F:XontoYF:XY
65 fdm F:XYdomF=X
66 63 64 65 3syl JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=sdomF=X
67 simprr JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=sJ=s
68 62 66 67 3eqtr3d JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=sX=s
69 68 imaeq2d JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=sFX=Fs
70 foima F:XontoYFX=Y
71 63 70 syl JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=sFX=Y
72 50 ralrimiva JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=scsFcu
73 dfiun2g csFcucsFc=d|csd=Fc
74 72 73 syl JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=scsFc=d|csd=Fc
75 imauni Fs=csFc
76 55 unieqi rancsFc=d|csd=Fc
77 74 75 76 3eqtr4g JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=sFs=rancsFc
78 69 71 77 3eqtr3d JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=sY=rancsFc
79 unieq v=rancsFcv=rancsFc
80 79 rspceeqv rancsFc𝒫uFinY=rancsFcv𝒫uFinY=v
81 60 78 80 syl2anc JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=sv𝒫uFinY=v
82 81 expr JCompF:XontoYFJCnKuKY=usranyuF-1ysFinJ=sv𝒫uFinY=v
83 31 82 sylan2b JCompF:XontoYFJCnKuKY=us𝒫ranyuF-1yFinJ=sv𝒫uFinY=v
84 83 rexlimdva JCompF:XontoYFJCnKuKY=us𝒫ranyuF-1yFinJ=sv𝒫uFinY=v
85 30 84 mpd JCompF:XontoYFJCnKuKY=uv𝒫uFinY=v
86 85 expr JCompF:XontoYFJCnKuKY=uv𝒫uFinY=v
87 4 86 sylan2 JCompF:XontoYFJCnKu𝒫KY=uv𝒫uFinY=v
88 87 ralrimiva JCompF:XontoYFJCnKu𝒫KY=uv𝒫uFinY=v
89 1 iscmp KCompKTopu𝒫KY=uv𝒫uFinY=v
90 3 88 89 sylanbrc JCompF:XontoYFJCnKKComp