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 F V Fun F F = dom F

Proof

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