Theorem hashfundm

Description: The size of a set function is equal to the size of its domain. (Contributed by BTernaryTau, 30-Sep-2023)

	Ref	Expression
Assertion	hashfundm	⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		hashfun	⊢ ( 𝐹 ∈ Fin → ( Fun 𝐹 ↔ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) ) )
2	1	biimpd	⊢ ( 𝐹 ∈ Fin → ( Fun 𝐹 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) ) )
3	2	adantld	⊢ ( 𝐹 ∈ Fin → ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) ) )
4		hashinf	⊢ ( ( 𝐹 ∈ 𝑉 ∧ ¬ 𝐹 ∈ Fin ) → ( ♯ ‘ 𝐹 ) = +∞ )
5	4	3adant2	⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ∧ ¬ 𝐹 ∈ Fin ) → ( ♯ ‘ 𝐹 ) = +∞ )
6		fundmfibi	⊢ ( Fun 𝐹 → ( 𝐹 ∈ Fin ↔ dom 𝐹 ∈ Fin ) )
7	6	notbid	⊢ ( Fun 𝐹 → ( ¬ 𝐹 ∈ Fin ↔ ¬ dom 𝐹 ∈ Fin ) )
8	7	adantl	⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ¬ 𝐹 ∈ Fin ↔ ¬ dom 𝐹 ∈ Fin ) )
9		dmexg	⊢ ( 𝐹 ∈ 𝑉 → dom 𝐹 ∈ V )
10		hashinf	⊢ ( ( dom 𝐹 ∈ V ∧ ¬ dom 𝐹 ∈ Fin ) → ( ♯ ‘ dom 𝐹 ) = +∞ )
11	9 10	sylan	⊢ ( ( 𝐹 ∈ 𝑉 ∧ ¬ dom 𝐹 ∈ Fin ) → ( ♯ ‘ dom 𝐹 ) = +∞ )
12	11	ex	⊢ ( 𝐹 ∈ 𝑉 → ( ¬ dom 𝐹 ∈ Fin → ( ♯ ‘ dom 𝐹 ) = +∞ ) )
13	12	adantr	⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ¬ dom 𝐹 ∈ Fin → ( ♯ ‘ dom 𝐹 ) = +∞ ) )
14	8 13	sylbid	⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ¬ 𝐹 ∈ Fin → ( ♯ ‘ dom 𝐹 ) = +∞ ) )
15	14	3impia	⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ∧ ¬ 𝐹 ∈ Fin ) → ( ♯ ‘ dom 𝐹 ) = +∞ )
16	5 15	eqtr4d	⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ∧ ¬ 𝐹 ∈ Fin ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) )
17	16	3comr	⊢ ( ( ¬ 𝐹 ∈ Fin ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) )
18	17	3expib	⊢ ( ¬ 𝐹 ∈ Fin → ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) ) )
19	3 18	pm2.61i	⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) )