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