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 e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) -> ( C e. J <-> C e. ( J |`t A ) ) )

Proof

Step Hyp Ref Expression
1 simpr3 
 |-  ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) -> C C_ B )
2 simpr2 
 |-  ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) -> B C_ A )
3 1 2 sstrd 
 |-  ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) -> C C_ A )
4 df-ss 
 |-  ( C C_ A <-> ( C i^i A ) = C )
5 3 4 sylib 
 |-  ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) -> ( C i^i A ) = C )
6 5 eqcomd 
 |-  ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) -> C = ( C i^i A ) )
7 ineq1 
 |-  ( v = C -> ( v i^i A ) = ( C i^i A ) )
8 7 rspceeqv 
 |-  ( ( C e. J /\ C = ( C i^i A ) ) -> E. v e. J C = ( v i^i A ) )
9 8 expcom 
 |-  ( C = ( C i^i A ) -> ( C e. J -> E. v e. J C = ( v i^i A ) ) )
10 6 9 syl 
 |-  ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) -> ( C e. J -> E. v e. J C = ( v i^i A ) ) )
11 inass 
 |-  ( ( v i^i A ) i^i B ) = ( v i^i ( A i^i B ) )
12 simprr 
 |-  ( ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) /\ ( v e. J /\ C = ( v i^i A ) ) ) -> C = ( v i^i A ) )
13 12 ineq1d 
 |-  ( ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) /\ ( v e. J /\ C = ( v i^i A ) ) ) -> ( C i^i B ) = ( ( v i^i A ) i^i B ) )
14 simplr3 
 |-  ( ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) /\ v e. J ) -> C C_ B )
15 df-ss 
 |-  ( C C_ B <-> ( C i^i B ) = C )
16 14 15 sylib 
 |-  ( ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) /\ v e. J ) -> ( C i^i B ) = C )
17 16 adantrr 
 |-  ( ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) /\ ( v e. J /\ C = ( v i^i A ) ) ) -> ( C i^i B ) = C )
18 13 17 eqtr3d 
 |-  ( ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) /\ ( v e. J /\ C = ( v i^i A ) ) ) -> ( ( v i^i A ) i^i B ) = C )
19 simplr2 
 |-  ( ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) /\ v e. J ) -> B C_ A )
20 sseqin2 
 |-  ( B C_ A <-> ( A i^i B ) = B )
21 19 20 sylib 
 |-  ( ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) /\ v e. J ) -> ( A i^i B ) = B )
22 21 ineq2d 
 |-  ( ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) /\ v e. J ) -> ( v i^i ( A i^i B ) ) = ( v i^i B ) )
23 22 adantrr 
 |-  ( ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) /\ ( v e. J /\ C = ( v i^i A ) ) ) -> ( v i^i ( A i^i B ) ) = ( v i^i B ) )
24 11 18 23 3eqtr3a 
 |-  ( ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) /\ ( v e. J /\ C = ( v i^i A ) ) ) -> C = ( v i^i B ) )
25 simplll 
 |-  ( ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) /\ ( v e. J /\ C = ( v i^i A ) ) ) -> J e. Top )
26 simprl 
 |-  ( ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) /\ ( v e. J /\ C = ( v i^i A ) ) ) -> v e. J )
27 simplr1 
 |-  ( ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) /\ ( v e. J /\ C = ( v i^i A ) ) ) -> B e. J )
28 inopn 
 |-  ( ( J e. Top /\ v e. J /\ B e. J ) -> ( v i^i B ) e. J )
29 25 26 27 28 syl3anc 
 |-  ( ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) /\ ( v e. J /\ C = ( v i^i A ) ) ) -> ( v i^i B ) e. J )
30 24 29 eqeltrd 
 |-  ( ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) /\ ( v e. J /\ C = ( v i^i A ) ) ) -> C e. J )
31 30 rexlimdvaa 
 |-  ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) -> ( E. v e. J C = ( v i^i A ) -> C e. J ) )
32 10 31 impbid 
 |-  ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) -> ( C e. J <-> E. v e. J C = ( v i^i A ) ) )
33 elrest 
 |-  ( ( J e. Top /\ A e. V ) -> ( C e. ( J |`t A ) <-> E. v e. J C = ( v i^i A ) ) )
34 33 adantr 
 |-  ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) -> ( C e. ( J |`t A ) <-> E. v e. J C = ( v i^i A ) ) )
35 32 34 bitr4d 
 |-  ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) -> ( C e. J <-> C e. ( J |`t A ) ) )