Theorem restsn2

Description: The subspace topology induced by a singleton. (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 16-Sep-2015)

	Ref	Expression
Assertion	restsn2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t { 𝐴 } ) = 𝒫 { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		snssi	⊢ ( 𝐴 ∈ 𝑋 → { 𝐴 } ⊆ 𝑋 )
2		resttopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ { 𝐴 } ⊆ 𝑋 ) → ( 𝐽 ↾t { 𝐴 } ) ∈ ( TopOn ‘ { 𝐴 } ) )
3	1 2	sylan2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t { 𝐴 } ) ∈ ( TopOn ‘ { 𝐴 } ) )
4		topsn	⊢ ( ( 𝐽 ↾t { 𝐴 } ) ∈ ( TopOn ‘ { 𝐴 } ) → ( 𝐽 ↾t { 𝐴 } ) = 𝒫 { 𝐴 } )
5	3 4	syl	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t { 𝐴 } ) = 𝒫 { 𝐴 } )