Theorem subspopn

Description: An open set is open in the subspace topology. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 15-Dec-2013)

	Ref	Expression
Assertion	subspopn	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝐽 ∧ 𝐵 ⊆ 𝐴 ) ) → 𝐵 ∈ ( 𝐽 ↾t 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elrestr	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐽 ) → ( 𝐵 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) )
2		dfss2	⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ∩ 𝐴 ) = 𝐵 )
3		eleq1	⊢ ( ( 𝐵 ∩ 𝐴 ) = 𝐵 → ( ( 𝐵 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) ↔ 𝐵 ∈ ( 𝐽 ↾t 𝐴 ) ) )
4	2 3	sylbi	⊢ ( 𝐵 ⊆ 𝐴 → ( ( 𝐵 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) ↔ 𝐵 ∈ ( 𝐽 ↾t 𝐴 ) ) )
5	1 4	syl5ibcom	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐽 ) → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ ( 𝐽 ↾t 𝐴 ) ) )
6	5	3expa	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐵 ∈ 𝐽 ) → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ ( 𝐽 ↾t 𝐴 ) ) )
7	6	impr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝐽 ∧ 𝐵 ⊆ 𝐴 ) ) → 𝐵 ∈ ( 𝐽 ↾t 𝐴 ) )