Theorem restuni2

Description: The underlying set of a subspace topology. (Contributed by Mario Carneiro, 21-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		restin.1	|- X = U. J
2		simpl	|- ( ( J e. Top /\ A e. V ) -> J e. Top )
3		inss2	|- ( A i^i X ) C_ X
4	1	restuni	|- ( ( J e. Top /\ ( A i^i X ) C_ X ) -> ( A i^i X ) = U. ( J |`t ( A i^i X ) ) )
5	2 3 4	sylancl	|- ( ( J e. Top /\ A e. V ) -> ( A i^i X ) = U. ( J |`t ( A i^i X ) ) )
6	1	restin	|- ( ( J e. Top /\ A e. V ) -> ( J |`t A ) = ( J |`t ( A i^i X ) ) )
7	6	unieqd	|- ( ( J e. Top /\ A e. V ) -> U. ( J |`t A ) = U. ( J |`t ( A i^i X ) ) )
8	5 7	eqtr4d	|- ( ( J e. Top /\ A e. V ) -> ( A i^i X ) = U. ( J |`t A ) )