Theorem restuni6

Description: The underlying set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	restuni6.1	|- ( ph -> A e. V )
	restuni6.2	|- ( ph -> B e. W )
Assertion	restuni6	|- ( ph -> U. ( A |`t B ) = ( U. A i^i B ) )

Proof

Step	Hyp	Ref	Expression
1		restuni6.1	|- ( ph -> A e. V )
2		restuni6.2	|- ( ph -> B e. W )
3		eqid	|- U. A = U. A
4	3	restin	|- ( ( A e. V /\ B e. W ) -> ( A |`t B ) = ( A |`t ( B i^i U. A ) ) )
5	1 2 4	syl2anc	|- ( ph -> ( A |`t B ) = ( A |`t ( B i^i U. A ) ) )
6	5	unieqd	|- ( ph -> U. ( A |`t B ) = U. ( A |`t ( B i^i U. A ) ) )
7		inss2	|- ( B i^i U. A ) C_ U. A
8	7	a1i	|- ( ph -> ( B i^i U. A ) C_ U. A )
9	1 8	restuni4	|- ( ph -> U. ( A |`t ( B i^i U. A ) ) = ( B i^i U. A ) )
10		incom	|- ( B i^i U. A ) = ( U. A i^i B )
11	10	a1i	|- ( ph -> ( B i^i U. A ) = ( U. A i^i B ) )
12	6 9 11	3eqtrd	|- ( ph -> U. ( A |`t B ) = ( U. A i^i B ) )