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		df-ss	|- ( 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 ) )