This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hashresfn

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

Ref Expression
Assertion hashresfn 
|- ( # |` A ) Fn A

Proof

Step Hyp Ref Expression
1 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
2 ffn 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> # Fn _V )
3 fnresin2 
 |-  ( # Fn _V -> ( # |` ( A i^i _V ) ) Fn ( A i^i _V ) )
4 1 2 3 mp2b 
 |-  ( # |` ( A i^i _V ) ) Fn ( A i^i _V )
5 inv1 
 |-  ( A i^i _V ) = A
6 5 reseq2i 
 |-  ( # |` ( A i^i _V ) ) = ( # |` A )
7 fneq12 
 |-  ( ( ( # |` ( A i^i _V ) ) = ( # |` A ) /\ ( A i^i _V ) = A ) -> ( ( # |` ( A i^i _V ) ) Fn ( A i^i _V ) <-> ( # |` A ) Fn A ) )
8 6 5 7 mp2an 
 |-  ( ( # |` ( A i^i _V ) ) Fn ( A i^i _V ) <-> ( # |` A ) Fn A )
9 4 8 mpbi 
 |-  ( # |` A ) Fn A