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	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A \land C \in Fin) \to F [C] \approx C$

Proof

Step	Hyp	Ref	Expression
1		f1ores	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A) \to ({F ↾}_{C}) : C \underset{1-1 onto}{⟶} F [C]$
2		f1oenfi	$⊢ (C \in Fin \land ({F ↾}_{C}) : C \underset{1-1 onto}{⟶} F [C]) \to C \approx F [C]$
3		ensymfib	$⊢ C \in Fin \to (C \approx F [C] \leftrightarrow F [C] \approx C)$
4	3	adantr	$⊢ (C \in Fin \land ({F ↾}_{C}) : C \underset{1-1 onto}{⟶} F [C]) \to (C \approx F [C] \leftrightarrow F [C] \approx C)$
5	2 4	mpbid	$⊢ (C \in Fin \land ({F ↾}_{C}) : C \underset{1-1 onto}{⟶} F [C]) \to F [C] \approx C$
6	1 5	sylan2	$⊢ (C \in Fin \land (F : A \underset{1-1}{⟶} B \land C \subseteq A)) \to F [C] \approx C$
7	6	3impb	$⊢ (C \in Fin \land F : A \underset{1-1}{⟶} B \land C \subseteq A) \to F [C] \approx C$
8	7	3coml	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A \land C \in Fin) \to F [C] \approx C$

Metamath Proof Explorer

Theorem f1imaenfi

Proof