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 ‘ ( 𝐴 ∩ 𝑋 ) ) )