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

Metamath Proof Explorer

Theorem restsubel

Description: A subset belongs in the space it generates via restriction. (Contributed by Glauco Siliprandi, 21-Dec-2024)

Ref Expression
Hypotheses restsubel.1 
|- ( ph -> J e. V )
restsubel.2 
|- ( ph -> U. J e. J )
restsubel.3 
|- ( ph -> A C_ U. J )
Assertion restsubel 
|- ( ph -> A e. ( J |`t A ) )

Proof

Step Hyp Ref Expression
1 restsubel.1 
 |-  ( ph -> J e. V )
2 restsubel.2 
 |-  ( ph -> U. J e. J )
3 restsubel.3 
 |-  ( ph -> A C_ U. J )
4 ineq1 
 |-  ( x = U. J -> ( x i^i A ) = ( U. J i^i A ) )
5 4 eqeq2d 
 |-  ( x = U. J -> ( A = ( x i^i A ) <-> A = ( U. J i^i A ) ) )
6 5 adantl 
 |-  ( ( ph /\ x = U. J ) -> ( A = ( x i^i A ) <-> A = ( U. J i^i A ) ) )
7 incom 
 |-  ( U. J i^i A ) = ( A i^i U. J )
8 7 a1i 
 |-  ( ph -> ( U. J i^i A ) = ( A i^i U. J ) )
9 dfss2 
 |-  ( A C_ U. J <-> ( A i^i U. J ) = A )
10 3 9 sylib 
 |-  ( ph -> ( A i^i U. J ) = A )
11 8 10 eqtrd 
 |-  ( ph -> ( U. J i^i A ) = A )
12 11 eqcomd 
 |-  ( ph -> A = ( U. J i^i A ) )
13 2 6 12 rspcedvd 
 |-  ( ph -> E. x e. J A = ( x i^i A ) )
14 2 3 ssexd 
 |-  ( ph -> A e. _V )
15 elrest 
 |-  ( ( J e. V /\ A e. _V ) -> ( A e. ( J |`t A ) <-> E. x e. J A = ( x i^i A ) ) )
16 1 14 15 syl2anc 
 |-  ( ph -> ( A e. ( J |`t A ) <-> E. x e. J A = ( x i^i A ) ) )
17 13 16 mpbird 
 |-  ( ph -> A e. ( J |`t A ) )