Metamath Proof Explorer

Theorem restopnb

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

Ref Expression
Assertion restopnb ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B → C ∈ J ↔ C ∈ J ↾ 𝑡 A

Proof

Step Hyp Ref Expression
1 simpr3 ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B → C ⊆ B
2 simpr2 ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B → B ⊆ A
3 1 2 sstrd ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B → C ⊆ A
4 df-ss ⊢ C ⊆ A ↔ C ∩ A = C
5 3 4 sylib ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B → C ∩ A = C
6 5 eqcomd ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B → C = C ∩ A
7 ineq1 ⊢ v = C → v ∩ A = C ∩ A
8 7 rspceeqv ⊢ C ∈ J ∧ C = C ∩ A → ∃ v ∈ J C = v ∩ A
9 8 expcom ⊢ C = C ∩ A → C ∈ J → ∃ v ∈ J C = v ∩ A
10 6 9 syl ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B → C ∈ J → ∃ v ∈ J C = v ∩ A
11 inass ⊢ v ∩ A ∩ B = v ∩ A ∩ B
12 simprr ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B ∧ v ∈ J ∧ C = v ∩ A → C = v ∩ A
13 12 ineq1d ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B ∧ v ∈ J ∧ C = v ∩ A → C ∩ B = v ∩ A ∩ B
14 simplr3 ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B ∧ v ∈ J → C ⊆ B
15 df-ss ⊢ C ⊆ B ↔ C ∩ B = C
16 14 15 sylib ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B ∧ v ∈ J → C ∩ B = C
17 16 adantrr ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B ∧ v ∈ J ∧ C = v ∩ A → C ∩ B = C
18 13 17 eqtr3d ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B ∧ v ∈ J ∧ C = v ∩ A → v ∩ A ∩ B = C
19 simplr2 ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B ∧ v ∈ J → B ⊆ A
20 sseqin2 ⊢ B ⊆ A ↔ A ∩ B = B
21 19 20 sylib ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B ∧ v ∈ J → A ∩ B = B
22 21 ineq2d ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B ∧ v ∈ J → v ∩ A ∩ B = v ∩ B
23 22 adantrr ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B ∧ v ∈ J ∧ C = v ∩ A → v ∩ A ∩ B = v ∩ B
24 11 18 23 3eqtr3a ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B ∧ v ∈ J ∧ C = v ∩ A → C = v ∩ B
25 simplll ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B ∧ v ∈ J ∧ C = v ∩ A → J ∈ Top
26 simprl ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B ∧ v ∈ J ∧ C = v ∩ A → v ∈ J
27 simplr1 ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B ∧ v ∈ J ∧ C = v ∩ A → B ∈ J
28 inopn ⊢ J ∈ Top ∧ v ∈ J ∧ B ∈ J → v ∩ B ∈ J
29 25 26 27 28 syl3anc ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B ∧ v ∈ J ∧ C = v ∩ A → v ∩ B ∈ J
30 24 29 eqeltrd ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B ∧ v ∈ J ∧ C = v ∩ A → C ∈ J
31 30 rexlimdvaa ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B → ∃ v ∈ J C = v ∩ A → C ∈ J
32 10 31 impbid ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B → C ∈ J ↔ ∃ v ∈ J C = v ∩ A
33 elrest ⊢ J ∈ Top ∧ A ∈ V → C ∈ J ↾ 𝑡 A ↔ ∃ v ∈ J C = v ∩ A
34 33 adantr ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B → C ∈ J ↾ 𝑡 A ↔ ∃ v ∈ J C = v ∩ A
35 32 34 bitr4d ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J ∧ B ⊆ A ∧ C ⊆ B → C ∈ J ↔ C ∈ J ↾ 𝑡 A