f1imaen2g

Description: If a function is one-to-one, then the image of a subset of its domain under it is equinumerous to the subset. (This version of f1imaeng does not need ax-rep .) (Contributed by Mario Carneiro, 16-Nov-2014) (Revised by Mario Carneiro, 25-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		simprr	$⊢ ((F : A \underset{1-1}{⟶} B \land B \in V) \land (C \subseteq A \land C \in V)) \to C \in V$
2		simplr	$⊢ ((F : A \underset{1-1}{⟶} B \land B \in V) \land (C \subseteq A \land C \in V)) \to B \in V$
3		f1f	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
4		fimass	$⊢ F : A ⟶ B \to F [C] \subseteq B$
5	3 4	syl	$⊢ F : A \underset{1-1}{⟶} B \to F [C] \subseteq B$
6	5	ad2antrr	$⊢ ((F : A \underset{1-1}{⟶} B \land B \in V) \land (C \subseteq A \land C \in V)) \to F [C] \subseteq B$
7	2 6	ssexd	$⊢ ((F : A \underset{1-1}{⟶} B \land B \in V) \land (C \subseteq A \land C \in V)) \to F [C] \in V$
8		f1ores	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A) \to ({F ↾}_{C}) : C \underset{1-1 onto}{⟶} F [C]$
9	8	ad2ant2r	$⊢ ((F : A \underset{1-1}{⟶} B \land B \in V) \land (C \subseteq A \land C \in V)) \to ({F ↾}_{C}) : C \underset{1-1 onto}{⟶} F [C]$
10		f1oen2g	$⊢ (C \in V \land F [C] \in V \land ({F ↾}_{C}) : C \underset{1-1 onto}{⟶} F [C]) \to C \approx F [C]$
11	1 7 9 10	syl3anc	$⊢ ((F : A \underset{1-1}{⟶} B \land B \in V) \land (C \subseteq A \land C \in V)) \to C \approx F [C]$
12	11	ensymd	$⊢ ((F : A \underset{1-1}{⟶} B \land B \in V) \land (C \subseteq A \land C \in V)) \to F [C] \approx C$

Metamath Proof Explorer

Theorem f1imaen2g

Proof