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

Metamath Proof Explorer

Theorem hashimaf1

Description: Taking the image of a set by a one-to-one function does not affect size. (Contributed by Thierry Arnoux, 18-Jan-2026)

Ref Expression
Hypotheses hashimaf1.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝐵 )
hashimaf1.2 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
hashimaf1.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion hashimaf1 ( 𝜑 → ( ♯ ‘ ( 𝐹 “ 𝐶 ) ) = ( ♯ ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 hashimaf1.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝐵 )
2 hashimaf1.2 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
3 hashimaf1.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4 3 2 sselpwd ⊢ ( 𝜑 → 𝐶 ∈ 𝒫 𝐴 )
5 f1ores ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) )
6 1 2 5 syl2anc ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) )
7 f1oeng ⊢ ( ( 𝐶 ∈ 𝒫 𝐴 ∧ ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) ) → 𝐶 ≈ ( 𝐹 “ 𝐶 ) )
8 4 6 7 syl2anc ⊢ ( 𝜑 → 𝐶 ≈ ( 𝐹 “ 𝐶 ) )
9 8 ensymd ⊢ ( 𝜑 → ( 𝐹 “ 𝐶 ) ≈ 𝐶 )
10 hasheni ⊢ ( ( 𝐹 “ 𝐶 ) ≈ 𝐶 → ( ♯ ‘ ( 𝐹 “ 𝐶 ) ) = ( ♯ ‘ 𝐶 ) )
11 9 10 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐹 “ 𝐶 ) ) = ( ♯ ‘ 𝐶 ) )