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 → ( 𝑆𝑁 ) ≤ ( ! ‘ 𝑁 ) )