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 = U. K
Assertion cncmp 
|- ( ( J e. Comp /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> K e. Comp )

Proof

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