rneqdmfinf1o

Description: Any function from a finite set onto the same set must be a bijection. (Contributed by AV, 5-Jul-2021)

		Ref	Expression
	Assertion	rneqdmfinf1o	$⊢ (A \in Fin \land F Fn A \land ran F = A) \to F : A \underset{1-1 onto}{⟶} A$

Step	Hyp	Ref	Expression
1		dffn4	$⊢ F Fn A \leftrightarrow F : A \underset{onto}{⟶} ran F$
2	1	biimpi	$⊢ F Fn A \to F : A \underset{onto}{⟶} ran F$
3	2	3ad2ant2	$⊢ (A \in Fin \land F Fn A \land ran F = A) \to F : A \underset{onto}{⟶} ran F$
4		foeq3	$⊢ ran F = A \to (F : A \underset{onto}{⟶} ran F \leftrightarrow F : A \underset{onto}{⟶} A)$
5	4	3ad2ant3	$⊢ (A \in Fin \land F Fn A \land ran F = A) \to (F : A \underset{onto}{⟶} ran F \leftrightarrow F : A \underset{onto}{⟶} A)$
6	3 5	mpbid	$⊢ (A \in Fin \land F Fn A \land ran F = A) \to F : A \underset{onto}{⟶} A$
7		enrefg	$⊢ A \in Fin \to A \approx A$
8	7	3ad2ant1	$⊢ (A \in Fin \land F Fn A \land ran F = A) \to A \approx A$
9		simp1	$⊢ (A \in Fin \land F Fn A \land ran F = A) \to A \in Fin$
10		fofinf1o	$⊢ (F : A \underset{onto}{⟶} A \land A \approx A \land A \in Fin) \to F : A \underset{1-1 onto}{⟶} A$
11	6 8 9 10	syl3anc	$⊢ (A \in Fin \land F Fn A \land ran F = A) \to F : A \underset{1-1 onto}{⟶} A$

Metamath Proof Explorer