subfaclefac

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

	Ref	Expression
Hypotheses	derang.d	$⊢ D = (x \in Fin ⟼ \|\{f \| (f : x \underset{1-1 onto}{⟶} x \land \forall y \in x f (y) \neq y)\}\|)$
	subfac.n	$⊢ S = (n \in ℕ_{0} ⟼ D ((1 \dots n)))$
Assertion	subfaclefac	$⊢ N \in ℕ_{0} \to S (N) \leq N!$

Proof

Step	Hyp	Ref	Expression
1		derang.d	$⊢ D = (x \in Fin ⟼ \|\{f \| (f : x \underset{1-1 onto}{⟶} x \land \forall y \in x f (y) \neq y)\}\|)$
2		subfac.n	$⊢ S = (n \in ℕ_{0} ⟼ D ((1 \dots n)))$
3		anidm	$⊢ (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)) \leftrightarrow f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
4	3	abbii	$⊢ \{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))\} = \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
5		fzfid	$⊢ N \in ℕ_{0} \to (1 \dots N) \in Fin$
6		deranglem	$⊢ (1 \dots N) \in Fin \to \{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))\} \in Fin$
7	5 6	syl	$⊢ N \in ℕ_{0} \to \{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))\} \in Fin$
8	4 7	eqeltrrid	$⊢ N \in ℕ_{0} \to \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \in Fin$
9		simpl	$⊢ (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land \forall y \in (1 \dots N) f (y) \neq y) \to f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
10	9	ss2abi	$⊢ \{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land \forall y \in (1 \dots N) f (y) \neq y)\} \subseteq \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
11		ssdomg	$⊢ \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \in Fin \to (\{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land \forall y \in (1 \dots N) f (y) \neq y)\} \subseteq \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \to \{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land \forall y \in (1 \dots N) f (y) \neq y)\} ≼ \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
12	8 10 11	mpisyl	$⊢ N \in ℕ_{0} \to \{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land \forall y \in (1 \dots N) f (y) \neq y)\} ≼ \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
13		deranglem	$⊢ (1 \dots N) \in Fin \to \{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land \forall y \in (1 \dots N) f (y) \neq y)\} \in Fin$
14	5 13	syl	$⊢ N \in ℕ_{0} \to \{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land \forall y \in (1 \dots N) f (y) \neq y)\} \in Fin$
15		hashdom	$⊢ (\{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land \forall y \in (1 \dots N) f (y) \neq y)\} \in Fin \land \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \in Fin) \to (\|\{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land \forall y \in (1 \dots N) f (y) \neq y)\}\| \leq \|\{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}\| \leftrightarrow \{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land \forall y \in (1 \dots N) f (y) \neq y)\} ≼ \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
16	14 8 15	syl2anc	$⊢ N \in ℕ_{0} \to (\|\{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land \forall y \in (1 \dots N) f (y) \neq y)\}\| \leq \|\{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}\| \leftrightarrow \{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land \forall y \in (1 \dots N) f (y) \neq y)\} ≼ \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
17	12 16	mpbird	$⊢ N \in ℕ_{0} \to \|\{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land \forall y \in (1 \dots N) f (y) \neq y)\}\| \leq \|\{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}\|$
18	1 2	subfacval	$⊢ N \in ℕ_{0} \to S (N) = D ((1 \dots N))$
19	1	derangval	$⊢ (1 \dots N) \in Fin \to D ((1 \dots N)) = \|\{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land \forall y \in (1 \dots N) f (y) \neq y)\}\|$
20	5 19	syl	$⊢ N \in ℕ_{0} \to D ((1 \dots N)) = \|\{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land \forall y \in (1 \dots N) f (y) \neq y)\}\|$
21	18 20	eqtrd	$⊢ N \in ℕ_{0} \to S (N) = \|\{f \| (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land \forall y \in (1 \dots N) f (y) \neq y)\}\|$
22		hashfac	$⊢ (1 \dots N) \in Fin \to \|\{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}\| = \|(1 \dots N)\|!$
23	5 22	syl	$⊢ N \in ℕ_{0} \to \|\{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}\| = \|(1 \dots N)\|!$
24		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
25	24	fveq2d	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\|! = N!$
26	23 25	eqtr2d	$⊢ N \in ℕ_{0} \to N! = \|\{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}\|$
27	17 21 26	3brtr4d	$⊢ N \in ℕ_{0} \to S (N) \leq N!$

Metamath Proof Explorer

Theorem subfaclefac

Proof