This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 toptopon2 ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
11 10 birani ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
12 cntop1 ⊢ ( 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) → 𝐽 ∈ Top )
13 12 adantl ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝐽 ∈ Top )
14 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
15 13 14 sylib ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
16 inss2 ⊢ ( 𝐵 ∩ ∪ 𝐾 ) ⊆ ∪ 𝐾
17 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ ( 𝐵 ∩ ∪ 𝐾 ) ⊆ ∪ 𝐾 ) → ( 𝐾 ↾t ( 𝐵 ∩ ∪ 𝐾 ) ) ∈ ( TopOn ‘ ( 𝐵 ∩ ∪ 𝐾 ) ) )
18 11 16 17 sylancl ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → ( 𝐾 ↾t ( 𝐵 ∩ ∪ 𝐾 ) ) ∈ ( TopOn ‘ ( 𝐵 ∩ ∪ 𝐾 ) ) )
19 cnf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ ( 𝐾 ↾t ( 𝐵 ∩ ∪ 𝐾 ) ) ∈ ( TopOn ‘ ( 𝐵 ∩ ∪ 𝐾 ) ) ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t ( 𝐵 ∩ ∪ 𝐾 ) ) ) ) → 𝑓 : ∪ 𝐽 ⟶ ( 𝐵 ∩ ∪ 𝐾 ) )
20 15 18 9 19 syl3anc ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝑓 : ∪ 𝐽 ⟶ ( 𝐵 ∩ ∪ 𝐾 ) )
21 20 frnd ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → ran 𝑓 ⊆ ( 𝐵 ∩ ∪ 𝐾 ) )
22 16 a1i ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → ( 𝐵 ∩ ∪ 𝐾 ) ⊆ ∪ 𝐾 )
23 cnrest2 ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ ran 𝑓 ⊆ ( 𝐵 ∩ ∪ 𝐾 ) ∧ ( 𝐵 ∩ ∪ 𝐾 ) ⊆ ∪ 𝐾 ) → ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t ( 𝐵 ∩ ∪ 𝐾 ) ) ) ) )
24 11 21 22 23 syl3anc ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t ( 𝐵 ∩ ∪ 𝐾 ) ) ) ) )
25 9 24 mpbird ⊢ ( ( 𝐾 ∈ Top ∧ 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ) → 𝑓 ∈ ( 𝐽 Cn 𝐾 ) )
26 25 ex ⊢ ( 𝐾 ∈ Top → ( 𝑓 ∈ ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) → 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) )
27 26 ssrdv ⊢ ( 𝐾 ∈ Top → ( 𝐽 Cn ( 𝐾 ↾t 𝐵 ) ) ⊆ ( 𝐽 Cn 𝐾 ) )