# 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 syl5ibr ( ( 𝐽 ∈ 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 𝐴 ) ↔ ( 𝐵𝐽𝐵𝐴 ) ) )