Metamath Proof Explorer

Theorem rncmp

Description: The image of a compact set under a continuous function is compact. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion rncmp 
|- ( ( J e. Comp /\ F e. ( J Cn K ) ) -> ( K |`t ran F ) e. Comp )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( J e. Comp /\ F e. ( J Cn K ) ) -> J e. Comp )
2 eqid 
 |-  U. J = U. J
3 eqid 
 |-  U. K = U. K
4 2 3 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> U. K )
5 4 adantl 
 |-  ( ( J e. Comp /\ F e. ( J Cn K ) ) -> F : U. J --> U. K )
6 5 ffnd 
 |-  ( ( J e. Comp /\ F e. ( J Cn K ) ) -> F Fn U. J )
7 dffn4 
 |-  ( F Fn U. J <-> F : U. J -onto-> ran F )
8 6 7 sylib 
 |-  ( ( J e. Comp /\ F e. ( J Cn K ) ) -> F : U. J -onto-> ran F )
9 cntop2 
 |-  ( F e. ( J Cn K ) -> K e. Top )
10 9 adantl 
 |-  ( ( J e. Comp /\ F e. ( J Cn K ) ) -> K e. Top )
11 5 frnd 
 |-  ( ( J e. Comp /\ F e. ( J Cn K ) ) -> ran F C_ U. K )
12 3 restuni 
 |-  ( ( K e. Top /\ ran F C_ U. K ) -> ran F = U. ( K |`t ran F ) )
13 10 11 12 syl2anc 
 |-  ( ( J e. Comp /\ F e. ( J Cn K ) ) -> ran F = U. ( K |`t ran F ) )
14 foeq3 
 |-  ( ran F = U. ( K |`t ran F ) -> ( F : U. J -onto-> ran F <-> F : U. J -onto-> U. ( K |`t ran F ) ) )
15 13 14 syl 
 |-  ( ( J e. Comp /\ F e. ( J Cn K ) ) -> ( F : U. J -onto-> ran F <-> F : U. J -onto-> U. ( K |`t ran F ) ) )
16 8 15 mpbid 
 |-  ( ( J e. Comp /\ F e. ( J Cn K ) ) -> F : U. J -onto-> U. ( K |`t ran F ) )
17 simpr 
 |-  ( ( J e. Comp /\ F e. ( J Cn K ) ) -> F e. ( J Cn K ) )
18 toptopon2 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
19 10 18 sylib 
 |-  ( ( J e. Comp /\ F e. ( J Cn K ) ) -> K e. ( TopOn ` U. K ) )
20 ssidd 
 |-  ( ( J e. Comp /\ F e. ( J Cn K ) ) -> ran F C_ ran F )
21 cnrest2 
 |-  ( ( K e. ( TopOn ` U. K ) /\ ran F C_ ran F /\ ran F C_ U. K ) -> ( F e. ( J Cn K ) <-> F e. ( J Cn ( K |`t ran F ) ) ) )
22 19 20 11 21 syl3anc 
 |-  ( ( J e. Comp /\ F e. ( J Cn K ) ) -> ( F e. ( J Cn K ) <-> F e. ( J Cn ( K |`t ran F ) ) ) )
23 17 22 mpbid 
 |-  ( ( J e. Comp /\ F e. ( J Cn K ) ) -> F e. ( J Cn ( K |`t ran F ) ) )
24 eqid 
 |-  U. ( K |`t ran F ) = U. ( K |`t ran F )
25 24 cncmp 
 |-  ( ( J e. Comp /\ F : U. J -onto-> U. ( K |`t ran F ) /\ F e. ( J Cn ( K |`t ran F ) ) ) -> ( K |`t ran F ) e. Comp )
26 1 16 23 25 syl3anc 
 |-  ( ( J e. Comp /\ F e. ( J Cn K ) ) -> ( K |`t ran F ) e. Comp )