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