Metamath Proof Explorer


Theorem cnrest

Description: Continuity of a restriction from a subspace. (Contributed by Jeff Hankins, 11-Jul-2009) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypothesis cnrest.1 𝑋 = 𝐽
Assertion cnrest ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴𝑋 ) → ( 𝐹𝐴 ) ∈ ( ( 𝐽t 𝐴 ) Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 cnrest.1 𝑋 = 𝐽
2 eqid 𝐾 = 𝐾
3 1 2 cnf ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝑋 𝐾 )
4 3 adantr ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴𝑋 ) → 𝐹 : 𝑋 𝐾 )
5 simpr ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴𝑋 ) → 𝐴𝑋 )
6 4 5 fssresd ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴𝑋 ) → ( 𝐹𝐴 ) : 𝐴 𝐾 )
7 cnvresima ( ( 𝐹𝐴 ) “ 𝑜 ) = ( ( 𝐹𝑜 ) ∩ 𝐴 )
8 cntop1 ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
9 8 adantr ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴𝑋 ) → 𝐽 ∈ Top )
10 9 adantr ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴𝑋 ) ∧ 𝑜𝐾 ) → 𝐽 ∈ Top )
11 1 topopn ( 𝐽 ∈ Top → 𝑋𝐽 )
12 ssexg ( ( 𝐴𝑋𝑋𝐽 ) → 𝐴 ∈ V )
13 12 ancoms ( ( 𝑋𝐽𝐴𝑋 ) → 𝐴 ∈ V )
14 11 13 sylan ( ( 𝐽 ∈ Top ∧ 𝐴𝑋 ) → 𝐴 ∈ V )
15 8 14 sylan ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴𝑋 ) → 𝐴 ∈ V )
16 15 adantr ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴𝑋 ) ∧ 𝑜𝐾 ) → 𝐴 ∈ V )
17 cnima ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑜𝐾 ) → ( 𝐹𝑜 ) ∈ 𝐽 )
18 17 adantlr ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴𝑋 ) ∧ 𝑜𝐾 ) → ( 𝐹𝑜 ) ∈ 𝐽 )
19 elrestr ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ V ∧ ( 𝐹𝑜 ) ∈ 𝐽 ) → ( ( 𝐹𝑜 ) ∩ 𝐴 ) ∈ ( 𝐽t 𝐴 ) )
20 10 16 18 19 syl3anc ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴𝑋 ) ∧ 𝑜𝐾 ) → ( ( 𝐹𝑜 ) ∩ 𝐴 ) ∈ ( 𝐽t 𝐴 ) )
21 7 20 eqeltrid ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴𝑋 ) ∧ 𝑜𝐾 ) → ( ( 𝐹𝐴 ) “ 𝑜 ) ∈ ( 𝐽t 𝐴 ) )
22 21 ralrimiva ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴𝑋 ) → ∀ 𝑜𝐾 ( ( 𝐹𝐴 ) “ 𝑜 ) ∈ ( 𝐽t 𝐴 ) )
23 1 toptopon ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
24 8 23 sylib ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
25 resttopon ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴𝑋 ) → ( 𝐽t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
26 24 25 sylan ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴𝑋 ) → ( 𝐽t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
27 cntop2 ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
28 27 adantr ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴𝑋 ) → 𝐾 ∈ Top )
29 2 toptopon ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝐾 ) )
30 28 29 sylib ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴𝑋 ) → 𝐾 ∈ ( TopOn ‘ 𝐾 ) )
31 iscn ( ( ( 𝐽t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝐾 ) ) → ( ( 𝐹𝐴 ) ∈ ( ( 𝐽t 𝐴 ) Cn 𝐾 ) ↔ ( ( 𝐹𝐴 ) : 𝐴 𝐾 ∧ ∀ 𝑜𝐾 ( ( 𝐹𝐴 ) “ 𝑜 ) ∈ ( 𝐽t 𝐴 ) ) ) )
32 26 30 31 syl2anc ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴𝑋 ) → ( ( 𝐹𝐴 ) ∈ ( ( 𝐽t 𝐴 ) Cn 𝐾 ) ↔ ( ( 𝐹𝐴 ) : 𝐴 𝐾 ∧ ∀ 𝑜𝐾 ( ( 𝐹𝐴 ) “ 𝑜 ) ∈ ( 𝐽t 𝐴 ) ) ) )
33 6 22 32 mpbir2and ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴𝑋 ) → ( 𝐹𝐴 ) ∈ ( ( 𝐽t 𝐴 ) Cn 𝐾 ) )