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 ⊢ X = ⋃ J
Assertion cnrest ⊢ F ∈ J Cn K ∧ A ⊆ X → F ↾ A ∈ J ↾ 𝑡 A Cn K

Proof

Step Hyp Ref Expression
1 cnrest.1 ⊢ X = ⋃ J
2 eqid ⊢ ⋃ K = ⋃ K
3 1 2 cnf ⊢ F ∈ J Cn K → F : X ⟶ ⋃ K
4 3 adantr ⊢ F ∈ J Cn K ∧ A ⊆ X → F : X ⟶ ⋃ K
5 simpr ⊢ F ∈ J Cn K ∧ A ⊆ X → A ⊆ X
6 4 5 fssresd ⊢ F ∈ J Cn K ∧ A ⊆ X → F ↾ A : A ⟶ ⋃ K
7 cnvresima ⊢ F ↾ A -1 o = F -1 o ∩ A
8 cntop1 ⊢ F ∈ J Cn K → J ∈ Top
9 8 adantr ⊢ F ∈ J Cn K ∧ A ⊆ X → J ∈ Top
10 9 adantr ⊢ F ∈ J Cn K ∧ A ⊆ X ∧ o ∈ K → J ∈ Top
11 1 topopn ⊢ J ∈ Top → X ∈ J
12 ssexg ⊢ A ⊆ X ∧ X ∈ J → A ∈ V
13 12 ancoms ⊢ X ∈ J ∧ A ⊆ X → A ∈ V
14 11 13 sylan ⊢ J ∈ Top ∧ A ⊆ X → A ∈ V
15 8 14 sylan ⊢ F ∈ J Cn K ∧ A ⊆ X → A ∈ V
16 15 adantr ⊢ F ∈ J Cn K ∧ A ⊆ X ∧ o ∈ K → A ∈ V
17 cnima ⊢ F ∈ J Cn K ∧ o ∈ K → F -1 o ∈ J
18 17 adantlr ⊢ F ∈ J Cn K ∧ A ⊆ X ∧ o ∈ K → F -1 o ∈ J
19 elrestr ⊢ J ∈ Top ∧ A ∈ V ∧ F -1 o ∈ J → F -1 o ∩ A ∈ J ↾ 𝑡 A
20 10 16 18 19 syl3anc ⊢ F ∈ J Cn K ∧ A ⊆ X ∧ o ∈ K → F -1 o ∩ A ∈ J ↾ 𝑡 A
21 7 20 eqeltrid ⊢ F ∈ J Cn K ∧ A ⊆ X ∧ o ∈ K → F ↾ A -1 o ∈ J ↾ 𝑡 A
22 21 ralrimiva ⊢ F ∈ J Cn K ∧ A ⊆ X → ∀ o ∈ K F ↾ A -1 o ∈ J ↾ 𝑡 A
23 1 toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ X
24 8 23 sylib ⊢ F ∈ J Cn K → J ∈ TopOn ⁡ X
25 resttopon ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → J ↾ 𝑡 A ∈ TopOn ⁡ A
26 24 25 sylan ⊢ F ∈ J Cn K ∧ A ⊆ X → J ↾ 𝑡 A ∈ TopOn ⁡ A
27 cntop2 ⊢ F ∈ J Cn K → K ∈ Top
28 27 adantr ⊢ F ∈ J Cn K ∧ A ⊆ X → K ∈ Top
29 2 toptopon ⊢ K ∈ Top ↔ K ∈ TopOn ⁡ ⋃ K
30 28 29 sylib ⊢ F ∈ J Cn K ∧ A ⊆ X → K ∈ TopOn ⁡ ⋃ K
31 iscn ⊢ J ↾ 𝑡 A ∈ TopOn ⁡ A ∧ K ∈ TopOn ⁡ ⋃ K → F ↾ A ∈ J ↾ 𝑡 A Cn K ↔ F ↾ A : A ⟶ ⋃ K ∧ ∀ o ∈ K F ↾ A -1 o ∈ J ↾ 𝑡 A
32 26 30 31 syl2anc ⊢ F ∈ J Cn K ∧ A ⊆ X → F ↾ A ∈ J ↾ 𝑡 A Cn K ↔ F ↾ A : A ⟶ ⋃ K ∧ ∀ o ∈ K F ↾ A -1 o ∈ J ↾ 𝑡 A
33 6 22 32 mpbir2and ⊢ F ∈ J Cn K ∧ A ⊆ X → F ↾ A ∈ J ↾ 𝑡 A Cn K