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 ( 𝐴 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) = ( ! ‘ ( ♯ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 hashf1 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ) = ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · ( ( ♯ ‘ 𝐴 ) C ( ♯ ‘ 𝐴 ) ) ) )
2 1 anidms ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ) = ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · ( ( ♯ ‘ 𝐴 ) C ( ♯ ‘ 𝐴 ) ) ) )
3 enrefg ⊢ ( 𝐴 ∈ Fin → 𝐴 ≈ 𝐴 )
4 f1finf1o ⊢ ( ( 𝐴 ≈ 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝑓 : 𝐴 –1-1→ 𝐴 ↔ 𝑓 : 𝐴 –1-1-onto→ 𝐴 ) )
5 3 4 mpancom ⊢ ( 𝐴 ∈ Fin → ( 𝑓 : 𝐴 –1-1→ 𝐴 ↔ 𝑓 : 𝐴 –1-1-onto→ 𝐴 ) )
6 5 abbidv ⊢ ( 𝐴 ∈ Fin → { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } = { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } )
7 6 fveq2d ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ) = ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) )
8 hashcl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
9 bcnn ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐴 ) C ( ♯ ‘ 𝐴 ) ) = 1 )
10 8 9 syl ⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) C ( ♯ ‘ 𝐴 ) ) = 1 )
11 10 oveq2d ⊢ ( 𝐴 ∈ Fin → ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · ( ( ♯ ‘ 𝐴 ) C ( ♯ ‘ 𝐴 ) ) ) = ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · 1 ) )
12 8 faccld ⊢ ( 𝐴 ∈ Fin → ( ! ‘ ( ♯ ‘ 𝐴 ) ) ∈ ℕ )
13 12 nncnd ⊢ ( 𝐴 ∈ Fin → ( ! ‘ ( ♯ ‘ 𝐴 ) ) ∈ ℂ )
14 13 mulridd ⊢ ( 𝐴 ∈ Fin → ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · 1 ) = ( ! ‘ ( ♯ ‘ 𝐴 ) ) )
15 11 14 eqtrd ⊢ ( 𝐴 ∈ Fin → ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · ( ( ♯ ‘ 𝐴 ) C ( ♯ ‘ 𝐴 ) ) ) = ( ! ‘ ( ♯ ‘ 𝐴 ) ) )
16 2 7 15 3eqtr3d ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) = ( ! ‘ ( ♯ ‘ 𝐴 ) ) )