Theorem hashresfn

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

	Ref	Expression
Assertion	hashresfn	⊢ ( ♯ ↾ 𝐴 ) Fn 𝐴

Proof

Step	Hyp	Ref	Expression
1		hashf	⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
2		ffn	⊢ ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) → ♯ Fn V )
3		fnresin2	⊢ ( ♯ Fn V → ( ♯ ↾ ( 𝐴 ∩ V ) ) Fn ( 𝐴 ∩ V ) )
4	1 2 3	mp2b	⊢ ( ♯ ↾ ( 𝐴 ∩ V ) ) Fn ( 𝐴 ∩ V )
5		inv1	⊢ ( 𝐴 ∩ V ) = 𝐴
6	5	reseq2i	⊢ ( ♯ ↾ ( 𝐴 ∩ V ) ) = ( ♯ ↾ 𝐴 )
7		fneq12	⊢ ( ( ( ♯ ↾ ( 𝐴 ∩ V ) ) = ( ♯ ↾ 𝐴 ) ∧ ( 𝐴 ∩ V ) = 𝐴 ) → ( ( ♯ ↾ ( 𝐴 ∩ V ) ) Fn ( 𝐴 ∩ V ) ↔ ( ♯ ↾ 𝐴 ) Fn 𝐴 ) )
8	6 5 7	mp2an	⊢ ( ( ♯ ↾ ( 𝐴 ∩ V ) ) Fn ( 𝐴 ∩ V ) ↔ ( ♯ ↾ 𝐴 ) Fn 𝐴 )
9	4 8	mpbi	⊢ ( ♯ ↾ 𝐴 ) Fn 𝐴