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

Metamath Proof Explorer

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