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

Metamath Proof Explorer

Theorem resttopon2

Description: The underlying set of a subspace topology. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion resttopon2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ ( 𝐴 ∩ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
2 resttop ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Top )
3 1 2 sylan ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Top )
4 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
5 4 ineq2d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐴 ∩ 𝑋 ) = ( 𝐴 ∩ ∪ 𝐽 ) )
6 5 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∩ 𝑋 ) = ( 𝐴 ∩ ∪ 𝐽 ) )
7 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
8 7 restuni2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∩ ∪ 𝐽 ) = ∪ ( 𝐽 ↾t 𝐴 ) )
9 1 8 sylan ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∩ ∪ 𝐽 ) = ∪ ( 𝐽 ↾t 𝐴 ) )
10 6 9 eqtrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∩ 𝑋 ) = ∪ ( 𝐽 ↾t 𝐴 ) )
11 istopon ⊢ ( ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ ( 𝐴 ∩ 𝑋 ) ) ↔ ( ( 𝐽 ↾t 𝐴 ) ∈ Top ∧ ( 𝐴 ∩ 𝑋 ) = ∪ ( 𝐽 ↾t 𝐴 ) ) )
12 3 10 11 sylanbrc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ ( 𝐴 ∩ 𝑋 ) ) )