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

Metamath Proof Explorer

Theorem restopn2

Description: If A is open, then B is open in A iff it is an open subset of A . (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion restopn2 ⊢ J ∈ Top ∧ A ∈ J → B ∈ J ↾ 𝑡 A ↔ B ∈ J ∧ B ⊆ A

Proof

Step Hyp Ref Expression
1 elssuni ⊢ B ∈ J ↾ 𝑡 A → B ⊆ ⋃ J ↾ 𝑡 A
2 elssuni ⊢ A ∈ J → A ⊆ ⋃ J
3 eqid ⊢ ⋃ J = ⋃ J
4 3 restuni ⊢ J ∈ Top ∧ A ⊆ ⋃ J → A = ⋃ J ↾ 𝑡 A
5 2 4 sylan2 ⊢ J ∈ Top ∧ A ∈ J → A = ⋃ J ↾ 𝑡 A
6 5 sseq2d ⊢ J ∈ Top ∧ A ∈ J → B ⊆ A ↔ B ⊆ ⋃ J ↾ 𝑡 A
7 1 6 imbitrrid ⊢ J ∈ Top ∧ A ∈ J → B ∈ J ↾ 𝑡 A → B ⊆ A
8 7 pm4.71rd ⊢ J ∈ Top ∧ A ∈ J → B ∈ J ↾ 𝑡 A ↔ B ⊆ A ∧ B ∈ J ↾ 𝑡 A
9 simpll ⊢ J ∈ Top ∧ A ∈ J ∧ B ⊆ A → J ∈ Top
10 simplr ⊢ J ∈ Top ∧ A ∈ J ∧ B ⊆ A → A ∈ J
11 ssidd ⊢ J ∈ Top ∧ A ∈ J ∧ B ⊆ A → A ⊆ A
12 simpr ⊢ J ∈ Top ∧ A ∈ J ∧ B ⊆ A → B ⊆ A
13 restopnb ⊢ J ∈ Top ∧ A ∈ J ∧ A ∈ J ∧ A ⊆ A ∧ B ⊆ A → B ∈ J ↔ B ∈ J ↾ 𝑡 A
14 9 10 10 11 12 13 syl23anc ⊢ J ∈ Top ∧ A ∈ J ∧ B ⊆ A → B ∈ J ↔ B ∈ J ↾ 𝑡 A
15 14 pm5.32da ⊢ J ∈ Top ∧ A ∈ J → B ⊆ A ∧ B ∈ J ↔ B ⊆ A ∧ B ∈ J ↾ 𝑡 A
16 8 15 bitr4d ⊢ J ∈ Top ∧ A ∈ J → B ∈ J ↾ 𝑡 A ↔ B ⊆ A ∧ B ∈ J
17 16 biancomd ⊢ J ∈ Top ∧ A ∈ J → B ∈ J ↾ 𝑡 A ↔ B ∈ J ∧ B ⊆ A