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 J Comp F : X onto Y F J Cn K K Comp

Proof

Step Hyp Ref Expression
1 cncmp.2 Y = K
2 cntop2 F J Cn K K Top
3 2 3ad2ant3 J Comp F : X onto Y F J Cn K K Top
4 elpwi u 𝒫 K u K
5 simpl1 J Comp F : X onto Y F J Cn K u K Y = u J Comp
6 simpl3 J Comp F : X onto Y F J Cn K u K Y = u F J Cn K
7 simprl J Comp F : X onto Y F J Cn K u K Y = u u K
8 7 sselda J Comp F : X onto Y F J Cn K u K Y = u y u y K
9 cnima F J Cn K y K F -1 y J
10 6 8 9 syl2an2r J Comp F : X onto Y F J Cn K u K Y = u y u F -1 y J
11 10 fmpttd J Comp F : X onto Y F J Cn K u K Y = u y u F -1 y : u J
12 11 frnd J Comp F : X onto Y F J Cn K u K Y = u ran y u F -1 y J
13 simprr J Comp F : X onto Y F J Cn K u K Y = u Y = u
14 13 imaeq2d J Comp F : X onto Y F J Cn K u K Y = u F -1 Y = F -1 u
15 eqid J = J
16 15 1 cnf F J Cn K F : J Y
17 6 16 syl J Comp F : X onto Y F J Cn K u K Y = u F : J Y
18 fimacnv F : J Y F -1 Y = J
19 17 18 syl J Comp F : X onto Y F J Cn K u K Y = u F -1 Y = J
20 10 ralrimiva J Comp F : X onto Y F J Cn K u K Y = u y u F -1 y J
21 dfiun2g y u F -1 y J y u F -1 y = x | y u x = F -1 y
22 20 21 syl J Comp F : X onto Y F J Cn K u K Y = u y u F -1 y = x | y u x = F -1 y
23 imauni F -1 u = y u F -1 y
24 eqid y u F -1 y = y u F -1 y
25 24 rnmpt ran y u F -1 y = x | y u x = F -1 y
26 25 unieqi ran y u F -1 y = x | y u x = F -1 y
27 22 23 26 3eqtr4g J Comp F : X onto Y F J Cn K u K Y = u F -1 u = ran y u F -1 y
28 14 19 27 3eqtr3d J Comp F : X onto Y F J Cn K u K Y = u J = ran y u F -1 y
29 15 cmpcov J Comp ran y u F -1 y J J = ran y u F -1 y s 𝒫 ran y u F -1 y Fin J = s
30 5 12 28 29 syl3anc J Comp F : X onto Y F J Cn K u K Y = u s 𝒫 ran y u F -1 y Fin J = s
31 elfpw s 𝒫 ran y u F -1 y Fin s ran y u F -1 y s Fin
32 simprll J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s s ran y u F -1 y
33 32 sselda J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s c s c ran y u F -1 y
34 simpll2 J Comp F : X onto Y F J Cn K u K Y = u y u F : X onto Y
35 elssuni y K y K
36 35 1 sseqtrrdi y K y Y
37 8 36 syl J Comp F : X onto Y F J Cn K u K Y = u y u y Y
38 foimacnv F : X onto Y y Y F F -1 y = y
39 34 37 38 syl2anc J Comp F : X onto Y F J Cn K u K Y = u y u F F -1 y = y
40 simpr J Comp F : X onto Y F J Cn K u K Y = u y u y u
41 39 40 eqeltrd J Comp F : X onto Y F J Cn K u K Y = u y u F F -1 y u
42 41 ralrimiva J Comp F : X onto Y F J Cn K u K Y = u y u F F -1 y u
43 imaeq2 c = F -1 y F c = F F -1 y
44 43 eleq1d c = F -1 y F c u F F -1 y u
45 24 44 ralrnmptw y u F -1 y J c ran y u F -1 y F c u y u F F -1 y u
46 20 45 syl J Comp F : X onto Y F J Cn K u K Y = u c ran y u F -1 y F c u y u F F -1 y u
47 42 46 mpbird J Comp F : X onto Y F J Cn K u K Y = u c ran y u F -1 y F c u
48 47 adantr J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s c ran y u F -1 y F c u
49 48 r19.21bi J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s c ran y u F -1 y F c u
50 33 49 syldan J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s c s F c u
51 50 fmpttd J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s c s F c : s u
52 51 frnd J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s ran c s F c u
53 simprlr J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s s Fin
54 eqid c s F c = c s F c
55 54 rnmpt ran c s F c = d | c s d = F c
56 abrexfi s Fin d | c s d = F c Fin
57 55 56 eqeltrid s Fin ran c s F c Fin
58 53 57 syl J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s ran c s F c Fin
59 elfpw ran c s F c 𝒫 u Fin ran c s F c u ran c s F c Fin
60 52 58 59 sylanbrc J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s ran c s F c 𝒫 u Fin
61 17 adantr J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s F : J Y
62 61 fdmd J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s dom F = J
63 simpll2 J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s F : X onto Y
64 fof F : X onto Y F : X Y
65 fdm F : X Y dom F = X
66 63 64 65 3syl J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s dom F = X
67 simprr J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s J = s
68 62 66 67 3eqtr3d J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s X = s
69 68 imaeq2d J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s F X = F s
70 foima F : X onto Y F X = Y
71 63 70 syl J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s F X = Y
72 50 ralrimiva J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s c s F c u
73 dfiun2g c s F c u c s F c = d | c s d = F c
74 72 73 syl J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s c s F c = d | c s d = F c
75 imauni F s = c s F c
76 55 unieqi ran c s F c = d | c s d = F c
77 74 75 76 3eqtr4g J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s F s = ran c s F c
78 69 71 77 3eqtr3d J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s Y = ran c s F c
79 unieq v = ran c s F c v = ran c s F c
80 79 rspceeqv ran c s F c 𝒫 u Fin Y = ran c s F c v 𝒫 u Fin Y = v
81 60 78 80 syl2anc J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s v 𝒫 u Fin Y = v
82 81 expr J Comp F : X onto Y F J Cn K u K Y = u s ran y u F -1 y s Fin J = s v 𝒫 u Fin Y = v
83 31 82 sylan2b J Comp F : X onto Y F J Cn K u K Y = u s 𝒫 ran y u F -1 y Fin J = s v 𝒫 u Fin Y = v
84 83 rexlimdva J Comp F : X onto Y F J Cn K u K Y = u s 𝒫 ran y u F -1 y Fin J = s v 𝒫 u Fin Y = v
85 30 84 mpd J Comp F : X onto Y F J Cn K u K Y = u v 𝒫 u Fin Y = v
86 85 expr J Comp F : X onto Y F J Cn K u K Y = u v 𝒫 u Fin Y = v
87 4 86 sylan2 J Comp F : X onto Y F J Cn K u 𝒫 K Y = u v 𝒫 u Fin Y = v
88 87 ralrimiva J Comp F : X onto Y F J Cn K u 𝒫 K Y = u v 𝒫 u Fin Y = v
89 1 iscmp K Comp K Top u 𝒫 K Y = u v 𝒫 u Fin Y = v
90 3 88 89 sylanbrc J Comp F : X onto Y F J Cn K K Comp