Theorem restuni4

Description: The underlying set of a subspace induced by the ` |``t ` operator. The result can be applied, for instance, to topologies and sigma-algebras. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	restuni4.1	|- ( ph -> A e. V )
	restuni4.2	|- ( ph -> B C_ U. A )
Assertion	restuni4	|- ( ph -> U. ( A |`t B ) = B )

Proof

Step	Hyp	Ref	Expression
1		restuni4.1	|- ( ph -> A e. V )
2		restuni4.2	|- ( ph -> B C_ U. A )
3		incom	|- ( B i^i U. A ) = ( U. A i^i B )
4	3	a1i	|- ( ph -> ( B i^i U. A ) = ( U. A i^i B ) )
5		dfss	|- ( B C_ U. A <-> B = ( B i^i U. A ) )
6	2 5	sylib	|- ( ph -> B = ( B i^i U. A ) )
7	1	uniexd	|- ( ph -> U. A e. _V )
8	7 2	ssexd	|- ( ph -> B e. _V )
9	1 8	restuni3	|- ( ph -> U. ( A |`t B ) = ( U. A i^i B ) )
10	4 6 9	3eqtr4rd	|- ( ph -> U. ( A |`t B ) = B )