Theorem subsaluni

Description: A set belongs to the subspace sigma-algebra it induces. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	subsaluni.1	|- ( ph -> S e. SAlg )
	subsaluni.2	|- ( ph -> A C_ U. S )
Assertion	subsaluni	|- ( ph -> A e. ( S |`t A ) )

Proof

Step	Hyp	Ref	Expression
1		subsaluni.1	|- ( ph -> S e. SAlg )
2		subsaluni.2	|- ( ph -> A C_ U. S )
3	1 2	restuni4	|- ( ph -> U. ( S |`t A ) = A )
4	3	eqcomd	|- ( ph -> A = U. ( S |`t A ) )
5	1	uniexd	|- ( ph -> U. S e. _V )
6	5 2	ssexd	|- ( ph -> A e. _V )
7		eqid	|- ( S |`t A ) = ( S |`t A )
8	1 6 7	subsalsal	|- ( ph -> ( S |`t A ) e. SAlg )
9	8	salunid	|- ( ph -> U. ( S |`t A ) e. ( S |`t A ) )
10	4 9	eqeltrd	|- ( ph -> A e. ( S |`t A ) )