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 𝐾 ) )