Theorem 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	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐴 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dffn4	⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 –onto→ ran 𝐹 )
2	1	biimpi	⊢ ( 𝐹 Fn 𝐴 → 𝐹 : 𝐴 –onto→ ran 𝐹 )
3	2	3ad2ant2	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐴 ) → 𝐹 : 𝐴 –onto→ ran 𝐹 )
4		foeq3	⊢ ( ran 𝐹 = 𝐴 → ( 𝐹 : 𝐴 –onto→ ran 𝐹 ↔ 𝐹 : 𝐴 –onto→ 𝐴 ) )
5	4	3ad2ant3	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐴 ) → ( 𝐹 : 𝐴 –onto→ ran 𝐹 ↔ 𝐹 : 𝐴 –onto→ 𝐴 ) )
6	3 5	mpbid	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐴 ) → 𝐹 : 𝐴 –onto→ 𝐴 )
7		enrefg	⊢ ( 𝐴 ∈ Fin → 𝐴 ≈ 𝐴 )
8	7	3ad2ant1	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐴 ) → 𝐴 ≈ 𝐴 )
9		simp1	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐴 ) → 𝐴 ∈ Fin )
10		fofinf1o	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐴 ∧ 𝐴 ≈ 𝐴 ∧ 𝐴 ∈ Fin ) → 𝐹 : 𝐴 –1-1-onto→ 𝐴 )
11	6 8 9 10	syl3anc	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐴 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐴 )