Metamath Proof Explorer

Theorem resthauslem

Description: Lemma for resthaus and similar theorems. If the topological property A is preserved under injective preimages, then property A passes to subspaces. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypotheses resthauslem.1 ⊢ ( 𝐽 ∈ 𝐴 → 𝐽 ∈ Top )
resthauslem.2 ⊢ ( ( 𝐽 ∈ 𝐴 ∧ ( I ↾ ( 𝑆 ∩ ∪ 𝐽 ) ) : ( 𝑆 ∩ ∪ 𝐽 ) –1-1→ ( 𝑆 ∩ ∪ 𝐽 ) ∧ ( I ↾ ( 𝑆 ∩ ∪ 𝐽 ) ) ∈ ( ( 𝐽 ↾t 𝑆 ) Cn 𝐽 ) ) → ( 𝐽 ↾t 𝑆 ) ∈ 𝐴 )
Assertion resthauslem ( ( 𝐽 ∈ 𝐴 ∧ 𝑆 ∈ 𝑉 ) → ( 𝐽 ↾t 𝑆 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 resthauslem.1 ⊢ ( 𝐽 ∈ 𝐴 → 𝐽 ∈ Top )
2 resthauslem.2 ⊢ ( ( 𝐽 ∈ 𝐴 ∧ ( I ↾ ( 𝑆 ∩ ∪ 𝐽 ) ) : ( 𝑆 ∩ ∪ 𝐽 ) –1-1→ ( 𝑆 ∩ ∪ 𝐽 ) ∧ ( I ↾ ( 𝑆 ∩ ∪ 𝐽 ) ) ∈ ( ( 𝐽 ↾t 𝑆 ) Cn 𝐽 ) ) → ( 𝐽 ↾t 𝑆 ) ∈ 𝐴 )
3 simpl ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑆 ∈ 𝑉 ) → 𝐽 ∈ 𝐴 )
4 f1oi ⊢ ( I ↾ ( 𝑆 ∩ ∪ 𝐽 ) ) : ( 𝑆 ∩ ∪ 𝐽 ) –1-1-onto→ ( 𝑆 ∩ ∪ 𝐽 )
5 f1of1 ⊢ ( ( I ↾ ( 𝑆 ∩ ∪ 𝐽 ) ) : ( 𝑆 ∩ ∪ 𝐽 ) –1-1-onto→ ( 𝑆 ∩ ∪ 𝐽 ) → ( I ↾ ( 𝑆 ∩ ∪ 𝐽 ) ) : ( 𝑆 ∩ ∪ 𝐽 ) –1-1→ ( 𝑆 ∩ ∪ 𝐽 ) )
6 4 5 mp1i ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑆 ∈ 𝑉 ) → ( I ↾ ( 𝑆 ∩ ∪ 𝐽 ) ) : ( 𝑆 ∩ ∪ 𝐽 ) –1-1→ ( 𝑆 ∩ ∪ 𝐽 ) )
7 inss2 ⊢ ( 𝑆 ∩ ∪ 𝐽 ) ⊆ ∪ 𝐽
8 resabs1 ⊢ ( ( 𝑆 ∩ ∪ 𝐽 ) ⊆ ∪ 𝐽 → ( ( I ↾ ∪ 𝐽 ) ↾ ( 𝑆 ∩ ∪ 𝐽 ) ) = ( I ↾ ( 𝑆 ∩ ∪ 𝐽 ) ) )
9 7 8 ax-mp ⊢ ( ( I ↾ ∪ 𝐽 ) ↾ ( 𝑆 ∩ ∪ 𝐽 ) ) = ( I ↾ ( 𝑆 ∩ ∪ 𝐽 ) )
10 1 adantr ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑆 ∈ 𝑉 ) → 𝐽 ∈ Top )
11 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
12 10 11 sylib ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑆 ∈ 𝑉 ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
13 idcn ⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( I ↾ ∪ 𝐽 ) ∈ ( 𝐽 Cn 𝐽 ) )
14 12 13 syl ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑆 ∈ 𝑉 ) → ( I ↾ ∪ 𝐽 ) ∈ ( 𝐽 Cn 𝐽 ) )
15 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
16 15 cnrest ⊢ ( ( ( I ↾ ∪ 𝐽 ) ∈ ( 𝐽 Cn 𝐽 ) ∧ ( 𝑆 ∩ ∪ 𝐽 ) ⊆ ∪ 𝐽 ) → ( ( I ↾ ∪ 𝐽 ) ↾ ( 𝑆 ∩ ∪ 𝐽 ) ) ∈ ( ( 𝐽 ↾t ( 𝑆 ∩ ∪ 𝐽 ) ) Cn 𝐽 ) )
17 14 7 16 sylancl ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑆 ∈ 𝑉 ) → ( ( I ↾ ∪ 𝐽 ) ↾ ( 𝑆 ∩ ∪ 𝐽 ) ) ∈ ( ( 𝐽 ↾t ( 𝑆 ∩ ∪ 𝐽 ) ) Cn 𝐽 ) )
18 9 17 eqeltrrid ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑆 ∈ 𝑉 ) → ( I ↾ ( 𝑆 ∩ ∪ 𝐽 ) ) ∈ ( ( 𝐽 ↾t ( 𝑆 ∩ ∪ 𝐽 ) ) Cn 𝐽 ) )
19 15 restin ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑆 ∈ 𝑉 ) → ( 𝐽 ↾t 𝑆 ) = ( 𝐽 ↾t ( 𝑆 ∩ ∪ 𝐽 ) ) )
20 19 oveq1d ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑆 ∈ 𝑉 ) → ( ( 𝐽 ↾t 𝑆 ) Cn 𝐽 ) = ( ( 𝐽 ↾t ( 𝑆 ∩ ∪ 𝐽 ) ) Cn 𝐽 ) )
21 18 20 eleqtrrd ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑆 ∈ 𝑉 ) → ( I ↾ ( 𝑆 ∩ ∪ 𝐽 ) ) ∈ ( ( 𝐽 ↾t 𝑆 ) Cn 𝐽 ) )
22 3 6 21 2 syl3anc ⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝑆 ∈ 𝑉 ) → ( 𝐽 ↾t 𝑆 ) ∈ 𝐴 )