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 toptopon2 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
11 10 birani 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> K e. ( TopOn ` U. K ) )
12 cntop1 
 |-  ( f e. ( J Cn ( K |`t B ) ) -> J e. Top )
13 12 adantl 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> J e. Top )
14 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
15 13 14 sylib 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> J e. ( TopOn ` U. J ) )
16 inss2 
 |-  ( B i^i U. K ) C_ U. K
17 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 ) ) )
18 11 16 17 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 ) ) )
19 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 ) )
20 15 18 9 19 syl3anc 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> f : U. J --> ( B i^i U. K ) )
21 20 frnd 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> ran f C_ ( B i^i U. K ) )
22 16 a1i 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> ( B i^i U. K ) C_ U. K )
23 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 ) ) ) ) )
24 11 21 22 23 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 ) ) ) ) )
25 9 24 mpbird 
 |-  ( ( K e. Top /\ f e. ( J Cn ( K |`t B ) ) ) -> f e. ( J Cn K ) )
26 25 ex 
 |-  ( K e. Top -> ( f e. ( J Cn ( K |`t B ) ) -> f e. ( J Cn K ) ) )
27 26 ssrdv 
 |-  ( K e. Top -> ( J Cn ( K |`t B ) ) C_ ( J Cn K ) )