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 ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ) → ( 𝐵 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ( 𝐵 ∈ 𝐽 ∧ 𝐵 ⊆ 𝐴 ) ) )

Proof

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