This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ 𝐴 )