Metamath Proof Explorer

Theorem subfaclefac

Description: The subfactorial is less than the factorial. (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypotheses derang.d ⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
subfac.n ⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
Assertion subfaclefac ( 𝑁 ∈ ℕ0 → ( 𝑆 ‘ 𝑁 ) ≤ ( ! ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 derang.d ⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
2 subfac.n ⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
3 anidm ⊢ ( ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) ↔ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
4 3 abbii ⊢ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) } = { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) }
5 fzfid ⊢ ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) ∈ Fin )
6 deranglem ⊢ ( ( 1 ... 𝑁 ) ∈ Fin → { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) } ∈ Fin )
7 5 6 syl ⊢ ( 𝑁 ∈ ℕ0 → { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) } ∈ Fin )
8 4 7 eqeltrrid ⊢ ( 𝑁 ∈ ℕ0 → { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ∈ Fin )
9 simpl ⊢ ( ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ∀ 𝑦 ∈ ( 1 ... 𝑁 ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) → 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
10 9 ss2abi ⊢ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ∀ 𝑦 ∈ ( 1 ... 𝑁 ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ⊆ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) }
11 ssdomg ⊢ ( { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ∈ Fin → ( { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ∀ 𝑦 ∈ ( 1 ... 𝑁 ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ⊆ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } → { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ∀ 𝑦 ∈ ( 1 ... 𝑁 ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ≼ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
12 8 10 11 mpisyl ⊢ ( 𝑁 ∈ ℕ0 → { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ∀ 𝑦 ∈ ( 1 ... 𝑁 ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ≼ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
13 deranglem ⊢ ( ( 1 ... 𝑁 ) ∈ Fin → { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ∀ 𝑦 ∈ ( 1 ... 𝑁 ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ∈ Fin )
14 5 13 syl ⊢ ( 𝑁 ∈ ℕ0 → { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ∀ 𝑦 ∈ ( 1 ... 𝑁 ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ∈ Fin )
15 hashdom ⊢ ( ( { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ∀ 𝑦 ∈ ( 1 ... 𝑁 ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ∈ Fin ∧ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ∈ Fin ) → ( ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ∀ 𝑦 ∈ ( 1 ... 𝑁 ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) ≤ ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) ↔ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ∀ 𝑦 ∈ ( 1 ... 𝑁 ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ≼ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
16 14 8 15 syl2anc ⊢ ( 𝑁 ∈ ℕ0 → ( ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ∀ 𝑦 ∈ ( 1 ... 𝑁 ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) ≤ ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) ↔ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ∀ 𝑦 ∈ ( 1 ... 𝑁 ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ≼ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
17 12 16 mpbird ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ∀ 𝑦 ∈ ( 1 ... 𝑁 ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) ≤ ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
18 1 2 subfacval ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑆 ‘ 𝑁 ) = ( 𝐷 ‘ ( 1 ... 𝑁 ) ) )
19 1 derangval ⊢ ( ( 1 ... 𝑁 ) ∈ Fin → ( 𝐷 ‘ ( 1 ... 𝑁 ) ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ∀ 𝑦 ∈ ( 1 ... 𝑁 ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
20 5 19 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐷 ‘ ( 1 ... 𝑁 ) ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ∀ 𝑦 ∈ ( 1 ... 𝑁 ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
21 18 20 eqtrd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑆 ‘ 𝑁 ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ∀ 𝑦 ∈ ( 1 ... 𝑁 ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
22 hashfac ⊢ ( ( 1 ... 𝑁 ) ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) = ( ! ‘ ( ♯ ‘ ( 1 ... 𝑁 ) ) ) )
23 5 22 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) = ( ! ‘ ( ♯ ‘ ( 1 ... 𝑁 ) ) ) )
24 hashfz1 ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
25 24 fveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ ( ♯ ‘ ( 1 ... 𝑁 ) ) ) = ( ! ‘ 𝑁 ) )
26 23 25 eqtr2d ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) = ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
27 17 21 26 3brtr4d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑆 ‘ 𝑁 ) ≤ ( ! ‘ 𝑁 ) )