This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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