Theorem hashf1dmcdm

Description: The size of the domain of a one-to-one set function is less than or equal to the size of its codomain, if it exists. (Contributed by BTernaryTau, 1-Oct-2023)

	Ref	Expression
Assertion	hashf1dmcdm	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		hashf1dmrn	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ran 𝐹 ) )
2	1	3adant2	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ran 𝐹 ) )
3		f1f	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
4		frn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ran 𝐹 ⊆ 𝐵 )
5		hashss	⊢ ( ( 𝐵 ∈ 𝑊 ∧ ran 𝐹 ⊆ 𝐵 ) → ( ♯ ‘ ran 𝐹 ) ≤ ( ♯ ‘ 𝐵 ) )
6	4 5	sylan2	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ♯ ‘ ran 𝐹 ) ≤ ( ♯ ‘ 𝐵 ) )
7	3 6	sylan2	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ♯ ‘ ran 𝐹 ) ≤ ( ♯ ‘ 𝐵 ) )
8	7	3adant1	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ♯ ‘ ran 𝐹 ) ≤ ( ♯ ‘ 𝐵 ) )
9	2 8	eqbrtrd	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) )