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	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐹 “ 𝐶 ) ) = ( ♯ ‘ 𝐶 ) )