Metamath Proof Explorer

Theorem cnrest2r

Description: Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 7-Jun-2014)

Ref Expression
Assertion cnrest2r 
|- ( K e. Top -> ( J Cn ( K |`t B ) ) C_ ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> f e. ( J Cn ( K |`t B ) ) )
2 cntop2 
 |-  ( f e. ( J Cn ( K |`t B ) ) -> ( K |`t B ) e. Top )
3 2 adantl 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> ( K |`t B ) e. Top )
4 restrcl 
 |-  ( ( K |`t B ) e. Top -> ( K e. _V /\ B e. _V ) )
5 eqid 
 |-  U. K = U. K
6 5 restin 
 |-  ( ( K e. _V /\ B e. _V ) -> ( K |`t B ) = ( K |`t ( B i^i U. K ) ) )
7 3 4 6 3syl 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> ( K |`t B ) = ( K |`t ( B i^i U. K ) ) )
8 7 oveq2d 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> ( J Cn ( K |`t B ) ) = ( J Cn ( K |`t ( B i^i U. K ) ) ) )
9 1 8 eleqtrd 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> f e. ( J Cn ( K |`t ( B i^i U. K ) ) ) )
10 simpl 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> K e. Top )
11 toptopon2 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
12 10 11 sylib 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> K e. ( TopOn ` U. K ) )
13 cntop1 
 |-  ( f e. ( J Cn ( K |`t B ) ) -> J e. Top )
14 13 adantl 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> J e. Top )
15 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
16 14 15 sylib 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> J e. ( TopOn ` U. J ) )
17 inss2 
 |-  ( B i^i U. K ) C_ U. K
18 resttopon 
 |-  ( ( K e. ( TopOn ` U. K ) /\ ( B i^i U. K ) C_ U. K ) -> ( K |`t ( B i^i U. K ) ) e. ( TopOn ` ( B i^i U. K ) ) )
19 12 17 18 sylancl 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> ( K |`t ( B i^i U. K ) ) e. ( TopOn ` ( B i^i U. K ) ) )
20 cnf2 
 |-  ( ( J e. ( TopOn ` U. J ) /\ ( K |`t ( B i^i U. K ) ) e. ( TopOn ` ( B i^i U. K ) ) /\ f e. ( J Cn ( K |`t ( B i^i U. K ) ) ) ) -> f : U. J --> ( B i^i U. K ) )
21 16 19 9 20 syl3anc 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> f : U. J --> ( B i^i U. K ) )
22 21 frnd 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> ran f C_ ( B i^i U. K ) )
23 17 a1i 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> ( B i^i U. K ) C_ U. K )
24 cnrest2 
 |-  ( ( K e. ( TopOn ` U. K ) /\ ran f C_ ( B i^i U. K ) /\ ( B i^i U. K ) C_ U. K ) -> ( f e. ( J Cn K ) <-> f e. ( J Cn ( K |`t ( B i^i U. K ) ) ) ) )
25 12 22 23 24 syl3anc 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> ( f e. ( J Cn K ) <-> f e. ( J Cn ( K |`t ( B i^i U. K ) ) ) ) )
26 9 25 mpbird 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> f e. ( J Cn K ) )
27 26 ex 
 |-  ( K e. Top -> ( f e. ( J Cn ( K |`t B ) ) -> f e. ( J Cn K ) ) )
28 27 ssrdv 
 |-  ( K e. Top -> ( J Cn ( K |`t B ) ) C_ ( J Cn K ) )