hashf1rn

Description: The size of a finite set which is a one-to-one function is equal to the size of the function's range. (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 4-May-2021)

		Ref	Expression
	Assertion	hashf1rn	$⊢ (A \in V \land F : A \underset{1-1}{⟶} B) \to \|F\| = \|ran F\|$

Proof

Step	Hyp	Ref	Expression
1		f1f	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
2	1	anim2i	$⊢ (A \in V \land F : A \underset{1-1}{⟶} B) \to (A \in V \land F : A ⟶ B)$
3	2	ancomd	$⊢ (A \in V \land F : A \underset{1-1}{⟶} B) \to (F : A ⟶ B \land A \in V)$
4		fex	$⊢ (F : A ⟶ B \land A \in V) \to F \in V$
5	3 4	syl	$⊢ (A \in V \land F : A \underset{1-1}{⟶} B) \to F \in V$
6		f1o2ndf1	$⊢ F : A \underset{1-1}{⟶} B \to ({2^{nd} ↾}_{F}) : F \underset{1-1 onto}{⟶} ran F$
7		df-2nd	$⊢ 2^{nd} = (x \in V ⟼ ⋃ ran \{x\})$
8	7	funmpt2	$⊢ Fun 2^{nd}$
9		resfunexg	$⊢ (Fun 2^{nd} \land F \in V) \to {2^{nd} ↾}_{F} \in V$
10	8 5 9	sylancr	$⊢ (A \in V \land F : A \underset{1-1}{⟶} B) \to {2^{nd} ↾}_{F} \in V$
11		f1oeq1	$⊢ {2^{nd} ↾}_{F} = f \to (({2^{nd} ↾}_{F}) : F \underset{1-1 onto}{⟶} ran F \leftrightarrow f : F \underset{1-1 onto}{⟶} ran F)$
12	11	biimpd	$⊢ {2^{nd} ↾}_{F} = f \to (({2^{nd} ↾}_{F}) : F \underset{1-1 onto}{⟶} ran F \to f : F \underset{1-1 onto}{⟶} ran F)$
13	12	eqcoms	$⊢ f = {2^{nd} ↾}_{F} \to (({2^{nd} ↾}_{F}) : F \underset{1-1 onto}{⟶} ran F \to f : F \underset{1-1 onto}{⟶} ran F)$
14	13	adantl	$⊢ ((A \in V \land F : A \underset{1-1}{⟶} B) \land f = {2^{nd} ↾}_{F}) \to (({2^{nd} ↾}_{F}) : F \underset{1-1 onto}{⟶} ran F \to f : F \underset{1-1 onto}{⟶} ran F)$
15	10 14	spcimedv	$⊢ (A \in V \land F : A \underset{1-1}{⟶} B) \to (({2^{nd} ↾}_{F}) : F \underset{1-1 onto}{⟶} ran F \to \exists f f : F \underset{1-1 onto}{⟶} ran F)$
16	15	ex	$⊢ A \in V \to (F : A \underset{1-1}{⟶} B \to (({2^{nd} ↾}_{F}) : F \underset{1-1 onto}{⟶} ran F \to \exists f f : F \underset{1-1 onto}{⟶} ran F))$
17	16	com13	$⊢ ({2^{nd} ↾}_{F}) : F \underset{1-1 onto}{⟶} ran F \to (F : A \underset{1-1}{⟶} B \to (A \in V \to \exists f f : F \underset{1-1 onto}{⟶} ran F))$
18	6 17	mpcom	$⊢ F : A \underset{1-1}{⟶} B \to (A \in V \to \exists f f : F \underset{1-1 onto}{⟶} ran F)$
19	18	impcom	$⊢ (A \in V \land F : A \underset{1-1}{⟶} B) \to \exists f f : F \underset{1-1 onto}{⟶} ran F$
20		hasheqf1oi	$⊢ F \in V \to (\exists f f : F \underset{1-1 onto}{⟶} ran F \to \|F\| = \|ran F\|)$
21	5 19 20	sylc	$⊢ (A \in V \land F : A \underset{1-1}{⟶} B) \to \|F\| = \|ran F\|$

Metamath Proof Explorer

Theorem hashf1rn

Proof