Theorem dmhashres

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

	Ref	Expression
Assertion	dmhashres	⊢ dom ( ♯ ↾ 𝐴 ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		dmres	⊢ dom ( ♯ ↾ 𝐴 ) = ( 𝐴 ∩ dom ♯ )
2		hashf	⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
3	2	fdmi	⊢ dom ♯ = V
4	3	ineq2i	⊢ ( 𝐴 ∩ dom ♯ ) = ( 𝐴 ∩ V )
5		inv1	⊢ ( 𝐴 ∩ V ) = 𝐴
6	1 4 5	3eqtri	⊢ dom ( ♯ ↾ 𝐴 ) = 𝐴