Step |
Hyp |
Ref |
Expression |
1 |
|
restin.1 |
|- X = U. J |
2 |
|
simpl |
|- ( ( J e. Top /\ A e. V ) -> J e. Top ) |
3 |
|
inss2 |
|- ( A i^i X ) C_ X |
4 |
1
|
restuni |
|- ( ( J e. Top /\ ( A i^i X ) C_ X ) -> ( A i^i X ) = U. ( J |`t ( A i^i X ) ) ) |
5 |
2 3 4
|
sylancl |
|- ( ( J e. Top /\ A e. V ) -> ( A i^i X ) = U. ( J |`t ( A i^i X ) ) ) |
6 |
1
|
restin |
|- ( ( J e. Top /\ A e. V ) -> ( J |`t A ) = ( J |`t ( A i^i X ) ) ) |
7 |
6
|
unieqd |
|- ( ( J e. Top /\ A e. V ) -> U. ( J |`t A ) = U. ( J |`t ( A i^i X ) ) ) |
8 |
5 7
|
eqtr4d |
|- ( ( J e. Top /\ A e. V ) -> ( A i^i X ) = U. ( J |`t A ) ) |