Theorem restval

Description: The subspace topology induced by the topology J on the set A . (Contributed by FL, 20-Sep-2010) (Revised by Mario Carneiro, 1-May-2015)

	Ref	Expression
Assertion	restval	|- ( ( J e. V /\ A e. W ) -> ( J |`t A ) = ran ( x e. J |-> ( x i^i A ) ) )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( J e. V -> J e. _V )
2		elex	|- ( A e. W -> A e. _V )
3		mptexg	|- ( J e. _V -> ( x e. J |-> ( x i^i A ) ) e. _V )
4		rnexg	|- ( ( x e. J |-> ( x i^i A ) ) e. _V -> ran ( x e. J |-> ( x i^i A ) ) e. _V )
5	3 4	syl	|- ( J e. _V -> ran ( x e. J |-> ( x i^i A ) ) e. _V )
6	5	adantr	|- ( ( J e. _V /\ A e. _V ) -> ran ( x e. J |-> ( x i^i A ) ) e. _V )
7		simpl	|- ( ( j = J /\ y = A ) -> j = J )
8		simpr	|- ( ( j = J /\ y = A ) -> y = A )
9	8	ineq2d	|- ( ( j = J /\ y = A ) -> ( x i^i y ) = ( x i^i A ) )
10	7 9	mpteq12dv	|- ( ( j = J /\ y = A ) -> ( x e. j |-> ( x i^i y ) ) = ( x e. J |-> ( x i^i A ) ) )
11	10	rneqd	|- ( ( j = J /\ y = A ) -> ran ( x e. j |-> ( x i^i y ) ) = ran ( x e. J |-> ( x i^i A ) ) )
12		df-rest	|- |`t = ( j e. _V , y e. _V |-> ran ( x e. j |-> ( x i^i y ) ) )
13	11 12	ovmpoga	|- ( ( J e. _V /\ A e. _V /\ ran ( x e. J |-> ( x i^i A ) ) e. _V ) -> ( J |`t A ) = ran ( x e. J |-> ( x i^i A ) ) )
14	6 13	mpd3an3	|- ( ( J e. _V /\ A e. _V ) -> ( J |`t A ) = ran ( x e. J |-> ( x i^i A ) ) )
15	1 2 14	syl2an	|- ( ( J e. V /\ A e. W ) -> ( J |`t A ) = ran ( x e. J |-> ( x i^i A ) ) )