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

Metamath Proof Explorer

Theorem hashf1dmrn

Description: The size of the domain of a one-to-one set function is equal to the size of its range. (Contributed by BTernaryTau, 1-Oct-2023)

Ref Expression
Assertion hashf1dmrn ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ran 𝐹 ) )

Proof

Step Hyp Ref Expression
1 f1fun ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → Fun 𝐹 )
2 hashfundm ⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) )
3 1 2 sylan2 ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) )
4 f1dm ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → dom 𝐹 = 𝐴 )
5 4 adantl ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → dom 𝐹 = 𝐴 )
6 dmexg ⊢ ( 𝐹 ∈ 𝑉 → dom 𝐹 ∈ V )
7 6 adantr ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → dom 𝐹 ∈ V )
8 5 7 eqeltrrd ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ∈ V )
9 hashf1rn ⊢ ( ( 𝐴 ∈ V ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ran 𝐹 ) )
10 8 9 sylancom ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ran 𝐹 ) )
11 5 fveq2d ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ♯ ‘ dom 𝐹 ) = ( ♯ ‘ 𝐴 ) )
12 3 10 11 3eqtr3rd ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ran 𝐹 ) )