Description: Restriction of the domain of the size function. (Contributed by Thierry Arnoux, 12-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | dmhashres | |- dom ( # |` A ) = A |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmres | |- dom ( # |` A ) = ( A i^i dom # ) |
|
2 | hashf | |- # : _V --> ( NN0 u. { +oo } ) |
|
3 | 2 | fdmi | |- dom # = _V |
4 | 3 | ineq2i | |- ( A i^i dom # ) = ( A i^i _V ) |
5 | inv1 | |- ( A i^i _V ) = A |
|
6 | 1 4 5 | 3eqtri | |- dom ( # |` A ) = A |