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

Metamath Proof Explorer

Theorem restin

Description: When the subspace region is not a subset of the base of the topology, the resulting set is the same as the subspace restricted to the base. (Contributed by Mario Carneiro, 15-Dec-2013)

		Ref	Expression
	Hypothesis	restin.1	\|- X = U. J
	Assertion	restin	\|- ( ( J e. V /\ A e. W ) -> ( J \|`t A ) = ( J \|`t ( A i^i X ) ) )

Proof

Step	Hyp	Ref	Expression
1		restin.1	\|- X = U. J
2		uniexg	\|- ( J e. V -> U. J e. _V )
3	1 2	eqeltrid	\|- ( J e. V -> X e. _V )
4	3	adantr	\|- ( ( J e. V /\ A e. W ) -> X e. _V )
5		restco	\|- ( ( J e. V /\ X e. _V /\ A e. W ) -> ( ( J \|`t X ) \|`t A ) = ( J \|`t ( X i^i A ) ) )
6	5	3com23	\|- ( ( J e. V /\ A e. W /\ X e. _V ) -> ( ( J \|`t X ) \|`t A ) = ( J \|`t ( X i^i A ) ) )
7	4 6	mpd3an3	\|- ( ( J e. V /\ A e. W ) -> ( ( J \|`t X ) \|`t A ) = ( J \|`t ( X i^i A ) ) )
8	1	restid	\|- ( J e. V -> ( J \|`t X ) = J )
9	8	adantr	\|- ( ( J e. V /\ A e. W ) -> ( J \|`t X ) = J )
10	9	oveq1d	\|- ( ( J e. V /\ A e. W ) -> ( ( J \|`t X ) \|`t A ) = ( J \|`t A ) )
11		incom	\|- ( X i^i A ) = ( A i^i X )
12	11	oveq2i	\|- ( J \|`t ( X i^i A ) ) = ( J \|`t ( A i^i X ) )
13	12	a1i	\|- ( ( J e. V /\ A e. W ) -> ( J \|`t ( X i^i A ) ) = ( J \|`t ( A i^i X ) ) )
14	7 10 13	3eqtr3d	\|- ( ( J e. V /\ A e. W ) -> ( J \|`t A ) = ( J \|`t ( A i^i X ) ) )