Metamath Proof Explorer


Theorem dmhashres

Description: Restriction of the domain of the size function. (Contributed by Thierry Arnoux, 12-Jan-2017)

Ref Expression
Assertion dmhashres
|- dom ( # |` A ) = A

Proof

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