Metamath Proof Explorer


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 𝐹 ) )