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 sseqin2 ⊢ ( 𝐴 ⊆ 𝑋 ↔ ( 𝑋 ∩ 𝐴 ) = 𝐴 )
9 8 bilani ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑋 ∩ 𝐴 ) = 𝐴 )
10 simpl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
11 3 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝑋 ∈ 𝐽 )
12 elrestr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ V ∧ 𝑋 ∈ 𝐽 ) → ( 𝑋 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) )
13 10 5 11 12 syl3anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑋 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) )
14 9 13 eqeltrrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ∈ ( 𝐽 ↾t 𝐴 ) )
15 elssuni ⊢ ( 𝐴 ∈ ( 𝐽 ↾t 𝐴 ) → 𝐴 ⊆ ∪ ( 𝐽 ↾t 𝐴 ) )
16 14 15 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ ∪ ( 𝐽 ↾t 𝐴 ) )
17 restval ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ V ) → ( 𝐽 ↾t 𝐴 ) = ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) )
18 5 17 syldan ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝐴 ) = ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) )
19 inss2 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴
20 vex ⊢ 𝑥 ∈ V
21 20 inex1 ⊢ ( 𝑥 ∩ 𝐴 ) ∈ V
22 21 elpw ⊢ ( ( 𝑥 ∩ 𝐴 ) ∈ 𝒫 𝐴 ↔ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 )
23 19 22 mpbir ⊢ ( 𝑥 ∩ 𝐴 ) ∈ 𝒫 𝐴
24 23 a1i ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝒫 𝐴 )
25 24 fmpttd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) : 𝐽 ⟶ 𝒫 𝐴 )
26 25 frnd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ran ( 𝑥 ∈ 𝐽 ↦ ( 𝑥 ∩ 𝐴 ) ) ⊆ 𝒫 𝐴 )
27 18 26 eqsstrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝐴 ) ⊆ 𝒫 𝐴 )
28 sspwuni ⊢ ( ( 𝐽 ↾t 𝐴 ) ⊆ 𝒫 𝐴 ↔ ∪ ( 𝐽 ↾t 𝐴 ) ⊆ 𝐴 )
29 27 28 sylib ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ∪ ( 𝐽 ↾t 𝐴 ) ⊆ 𝐴 )
30 16 29 eqssd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) )
31 istopon ⊢ ( ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ↔ ( ( 𝐽 ↾t 𝐴 ) ∈ Top ∧ 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) ) )
32 7 30 31 sylanbrc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )