Metamath Proof Explorer

Theorem resttopon

Description: A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion resttopon ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
2 id ⊢ ( 𝐴 ⊆ 𝑋 → 𝐴 ⊆ 𝑋 )
3 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
4 ssexg ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽 ) → 𝐴 ∈ V )
5 2 3 4 syl2anr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ∈ V )
6 resttop ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ V ) → ( 𝐽 ↾t 𝐴 ) ∈ Top )
7 1 5 6 syl2an2r ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝐴 ) ∈ Top )
8 simpr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ 𝑋 )
9 sseqin2 ⊢ ( 𝐴 ⊆ 𝑋 ↔ ( 𝑋 ∩ 𝐴 ) = 𝐴 )
10 8 9 sylib ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑋 ∩ 𝐴 ) = 𝐴 )
11 simpl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
12 3 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝑋 ∈ 𝐽 )
13 elrestr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ V ∧ 𝑋 ∈ 𝐽 ) → ( 𝑋 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) )
14 11 5 12 13 syl3anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑋 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) )
15 10 14 eqeltrrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ∈ ( 𝐽 ↾t 𝐴 ) )
16 elssuni ⊢ ( 𝐴 ∈ ( 𝐽 ↾t 𝐴 ) → 𝐴 ⊆ ∪ ( 𝐽 ↾t 𝐴 ) )
17 15 16 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ ∪ ( 𝐽 ↾t 𝐴 ) )
18 restval ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ V ) → ( 𝐽 ↾t 𝐴 ) = ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) )
19 5 18 syldan ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝐴 ) = ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) )
20 inss2 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴
21 vex ⊢ 𝑥 ∈ V
22 21 inex1 ⊢ ( 𝑥 ∩ 𝐴 ) ∈ V
23 22 elpw ⊢ ( ( 𝑥 ∩ 𝐴 ) ∈ 𝒫 𝐴 ↔ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 )
24 20 23 mpbir ⊢ ( 𝑥 ∩ 𝐴 ) ∈ 𝒫 𝐴
25 24 a1i ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝒫 𝐴 )
26 25 fmpttd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) : 𝐽 ⟶ 𝒫 𝐴 )
27 26 frnd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝒫 𝐴 )
28 19 27 eqsstrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝐴 ) ⊆ 𝒫 𝐴 )
29 sspwuni ⊢ ( ( 𝐽 ↾t 𝐴 ) ⊆ 𝒫 𝐴 ↔ ∪ ( 𝐽 ↾t 𝐴 ) ⊆ 𝐴 )
30 28 29 sylib ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ∪ ( 𝐽 ↾t 𝐴 ) ⊆ 𝐴 )
31 17 30 eqssd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) )
32 istopon ⊢ ( ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ↔ ( ( 𝐽 ↾t 𝐴 ) ∈ Top ∧ 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) ) )
33 7 31 32 sylanbrc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )