Theorem f1imaenfi

Description: If a function is one-to-one, then the image of a finite subset of its domain under it is equinumerous to the subset. This theorem is proved without using the Axiom of Replacement or the Axiom of Power Sets (unlike f1imaeng ). (Contributed by BTernaryTau, 29-Sep-2024)

	Ref	Expression
Assertion	f1imaenfi	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ Fin ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		f1ores	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) )
2		f1oenfi	⊢ ( ( 𝐶 ∈ Fin ∧ ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) ) → 𝐶 ≈ ( 𝐹 “ 𝐶 ) )
3		ensymfib	⊢ ( 𝐶 ∈ Fin → ( 𝐶 ≈ ( 𝐹 “ 𝐶 ) ↔ ( 𝐹 “ 𝐶 ) ≈ 𝐶 ) )
4	3	adantr	⊢ ( ( 𝐶 ∈ Fin ∧ ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) ) → ( 𝐶 ≈ ( 𝐹 “ 𝐶 ) ↔ ( 𝐹 “ 𝐶 ) ≈ 𝐶 ) )
5	2 4	mpbid	⊢ ( ( 𝐶 ∈ Fin ∧ ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 )
6	1 5	sylan2	⊢ ( ( 𝐶 ∈ Fin ∧ ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 )
7	6	3impb	⊢ ( ( 𝐶 ∈ Fin ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 )
8	7	3coml	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ Fin ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 )