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

Metamath Proof Explorer

Theorem hashfac

Description: A factorial counts the number of bijections on a finite set. (Contributed by Mario Carneiro, 21-Jan-2015) (Proof shortened by Mario Carneiro, 17-Apr-2015)

Ref Expression
Assertion hashfac ⊢ A ∈ Fin → f | f : A ⟶ 1-1 onto A = A !

Proof

Step Hyp Ref Expression
1 hashf1 ⊢ A ∈ Fin ∧ A ∈ Fin → f | f : A ⟶ 1-1 A = A ! ⁢ ( A A)
2 1 anidms ⊢ A ∈ Fin → f | f : A ⟶ 1-1 A = A ! ⁢ ( A A)
3 enrefg ⊢ A ∈ Fin → A ≈ A
4 f1finf1o ⊢ A ≈ A ∧ A ∈ Fin → f : A ⟶ 1-1 A ↔ f : A ⟶ 1-1 onto A
5 3 4 mpancom ⊢ A ∈ Fin → f : A ⟶ 1-1 A ↔ f : A ⟶ 1-1 onto A
6 5 abbidv ⊢ A ∈ Fin → f | f : A ⟶ 1-1 A = f | f : A ⟶ 1-1 onto A
7 6 fveq2d ⊢ A ∈ Fin → f | f : A ⟶ 1-1 A = f | f : A ⟶ 1-1 onto A
8 hashcl ⊢ A ∈ Fin → A ∈ ℕ 0
9 bcnn ⊢ A ∈ ℕ 0 → ( A A) = 1
10 8 9 syl ⊢ A ∈ Fin → ( A A) = 1
11 10 oveq2d ⊢ A ∈ Fin → A ! ⁢ ( A A) = A ! ⋅ 1
12 8 faccld ⊢ A ∈ Fin → A ! ∈ ℕ
13 12 nncnd ⊢ A ∈ Fin → A ! ∈ ℂ
14 13 mulridd ⊢ A ∈ Fin → A ! ⋅ 1 = A !
15 11 14 eqtrd ⊢ A ∈ Fin → A ! ⁢ ( A A) = A !
16 2 7 15 3eqtr3d ⊢ A ∈ Fin → f | f : A ⟶ 1-1 onto A = A !