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