This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elrestd

Description: A sufficient condition for being an open set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses elrestd.1 
|- ( ph -> J e. V )
elrestd.2 
|- ( ph -> B e. W )
elrestd.3 
|- ( ph -> X e. J )
elrestd.4 
|- A = ( X i^i B )
Assertion elrestd 
|- ( ph -> A e. ( J |`t B ) )

Proof

Step Hyp Ref Expression
1 elrestd.1 
 |-  ( ph -> J e. V )
2 elrestd.2 
 |-  ( ph -> B e. W )
3 elrestd.3 
 |-  ( ph -> X e. J )
4 elrestd.4 
 |-  A = ( X i^i B )
5 4 a1i 
 |-  ( ph -> A = ( X i^i B ) )
6 ineq1 
 |-  ( x = X -> ( x i^i B ) = ( X i^i B ) )
7 6 rspceeqv 
 |-  ( ( X e. J /\ A = ( X i^i B ) ) -> E. x e. J A = ( x i^i B ) )
8 3 5 7 syl2anc 
 |-  ( ph -> E. x e. J A = ( x i^i B ) )
9 elrest 
 |-  ( ( J e. V /\ B e. W ) -> ( A e. ( J |`t B ) <-> E. x e. J A = ( x i^i B ) ) )
10 1 2 9 syl2anc 
 |-  ( ph -> ( A e. ( J |`t B ) <-> E. x e. J A = ( x i^i B ) ) )
11 8 10 mpbird 
 |-  ( ph -> A e. ( J |`t B ) )