Metamath Proof Explorer


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 )