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 ) )