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 ) |
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 ) |