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