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

Proof

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