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 ( 𝐾 ∈ Top → ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ⊆ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) )
2 cntop2 ⊢ ( 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) → ( 𝐾 ↾t 𝐵 ) ∈ Top )
3 2 adantl ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → ( 𝐾 ↾t 𝐵 ) ∈ Top )
4 restrcl ⊢ ( ( 𝐾 ↾t 𝐵 ) ∈ Top → ( 𝐾 ∈ V ∧ 𝐵 ∈ V ) )
5 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
6 5 restin ⊢ ( ( 𝐾 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐾 ↾t 𝐵 ) = ( 𝐾 ↾t ( 𝐵 ∩ ∪ 𝐾 ) ) )
7 3 4 6 3syl ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → ( 𝐾 ↾t 𝐵 ) = ( 𝐾 ↾t ( 𝐵 ∩ ∪ 𝐾 ) ) )
8 7 oveq2d ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) = ( 𝐽 Cn ( 𝐾 ↾t ( 𝐵 ∩ ∪ 𝐾 ) ) ) )
9 1 8 eleqtrd ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t ( 𝐵 ∩ ∪ 𝐾 ) ) ) )
10 simpl ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝐾 ∈ Top )
11 toptopon2 ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
12 10 11 sylib ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
13 cntop1 ⊢ ( 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) → 𝐽 ∈ Top )
14 13 adantl ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝐽 ∈ Top )
15 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
16 14 15 sylib ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
17 inss2 ⊢ ( 𝐵 ∩ ∪ 𝐾 ) ⊆ ∪ 𝐾
18 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ ( 𝐵 ∩ ∪ 𝐾 ) ⊆ ∪ 𝐾 ) → ( 𝐾 ↾t ( 𝐵 ∩ ∪ 𝐾 ) ) ∈ ( TopOn ‘ ( 𝐵 ∩ ∪ 𝐾 ) ) )
19 12 17 18 sylancl ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → ( 𝐾 ↾t ( 𝐵 ∩ ∪ 𝐾 ) ) ∈ ( TopOn ‘ ( 𝐵 ∩ ∪ 𝐾 ) ) )
20 cnf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ ( 𝐾 ↾t ( 𝐵 ∩ ∪ 𝐾 ) ) ∈ ( TopOn ‘ ( 𝐵 ∩ ∪ 𝐾 ) ) ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t ( 𝐵 ∩ ∪ 𝐾 ) ) ) ) → 𝑓 : ∪ 𝐽 ⟶ ( 𝐵 ∩ ∪ 𝐾 ) )
21 16 19 9 20 syl3anc ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝑓 : ∪ 𝐽 ⟶ ( 𝐵 ∩ ∪ 𝐾 ) )
22 21 frnd ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → ran 𝑓 ⊆ ( 𝐵 ∩ ∪ 𝐾 ) )
23 17 a1i ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → ( 𝐵 ∩ ∪ 𝐾 ) ⊆ ∪ 𝐾 )
24 cnrest2 ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ ran 𝑓 ⊆ ( 𝐵 ∩ ∪ 𝐾 ) ∧ ( 𝐵 ∩ ∪ 𝐾 ) ⊆ ∪ 𝐾 ) → ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t ( 𝐵 ∩ ∪ 𝐾 ) ) ) ) )
25 12 22 23 24 syl3anc ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t ( 𝐵 ∩ ∪ 𝐾 ) ) ) ) )
26 9 25 mpbird ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝑓 ∈ ( 𝐽 Cn 𝐾 ) )
27 26 ex ⊢ ( 𝐾 ∈ Top → ( 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) → 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) )
28 27 ssrdv ⊢ ( 𝐾 ∈ Top → ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ⊆ ( 𝐽 Cn 𝐾 ) )