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 )