Metamath Proof Explorer

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 ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A → B ∈ J ↾ 𝑡 A

Proof

Step Hyp Ref Expression
1 elrestr ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J → B ∩ A ∈ J ↾ 𝑡 A
2 df-ss ⊢ B ⊆ A ↔ B ∩ A = B
3 eleq1 ⊢ B ∩ A = B → B ∩ A ∈ J ↾ 𝑡 A ↔ B ∈ J ↾ 𝑡 A
4 2 3 sylbi ⊢ B ⊆ A → B ∩ A ∈ J ↾ 𝑡 A ↔ B ∈ J ↾ 𝑡 A
5 1 4 syl5ibcom ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J → B ⊆ A → B ∈ J ↾ 𝑡 A
6 5 3expa ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J → B ⊆ A → B ∈ J ↾ 𝑡 A
7 6 impr ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A → B ∈ J ↾ 𝑡 A