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

Metamath Proof Explorer

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→ 𝐵 ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) )