Metamath Proof Explorer

Theorem f1imaen3g

Description: If a set function is one-to-one, then a subset of its domain is equinumerous to the image of that subset. (This version of f1imaeng does not need ax-rep nor ax-pow .) (Contributed by BTernaryTau, 13-Jan-2025)

		Ref	Expression
	Assertion	f1imaen3g	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A \land F \in V) \to C \approx F [C]$

Proof

Step	Hyp	Ref	Expression
1		resexg	$⊢ F \in V \to {F ↾}_{C} \in V$
2	1	3ad2ant3	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A \land F \in V) \to {F ↾}_{C} \in V$
3		f1ores	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A) \to ({F ↾}_{C}) : C \underset{1-1 onto}{⟶} F [C]$
4	3	3adant3	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A \land F \in V) \to ({F ↾}_{C}) : C \underset{1-1 onto}{⟶} F [C]$
5		f1oen3g	$⊢ ({F ↾}_{C} \in V \land ({F ↾}_{C}) : C \underset{1-1 onto}{⟶} F [C]) \to C \approx F [C]$
6	2 4 5	syl2anc	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A \land F \in V) \to C \approx F [C]$