Theorem restuni5

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
Hypothesis	restuni5.1	|- X = U. J
Assertion	restuni5	|- ( ( J e. V /\ A C_ X ) -> A = U. ( J |`t A ) )

Proof

Step	Hyp	Ref	Expression
1		restuni5.1	|- X = U. J
2		simpl	|- ( ( J e. V /\ A C_ X ) -> J e. V )
3		id	|- ( A C_ X -> A C_ X )
4	3 1	sseqtrdi	|- ( A C_ X -> A C_ U. J )
5	4	adantl	|- ( ( J e. V /\ A C_ X ) -> A C_ U. J )
6	2 5	restuni4	|- ( ( J e. V /\ A C_ X ) -> U. ( J |`t A ) = A )
7	6	eqcomd	|- ( ( J e. V /\ A C_ X ) -> A = U. ( J |`t A ) )