Theorem derangsn

Description: The derangement number of a singleton. (Contributed by Mario Carneiro, 19-Jan-2015)

	Ref	Expression
Hypothesis	derang.d	$$⊢D=\left(x\in \mathrm{Fin}⟼\left|\left\{f|\left(f:x\underset{1-1\; onto}{⟶}x\wedge \forall y\in xf\left(y\right)\ne y\right)\right\}\right|\right)$$
Assertion	derangsn	$$⊢A\in V\to D\left(\left\{A\right\}\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		derang.d	$$⊢D=\left(x\in \mathrm{Fin}⟼\left|\left\{f|\left(f:x\underset{1-1\; onto}{⟶}x\wedge \forall y\in xf\left(y\right)\ne y\right)\right\}\right|\right)$$
2		snfi	$$⊢\left\{A\right\}\in \mathrm{Fin}$$
3	1	derangval	$$⊢\left\{A\right\}\in \mathrm{Fin}\to D\left(\left\{A\right\}\right)=\left|\left\{f|\left(f:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\wedge \forall y\in \left\{A\right\}f\left(y\right)\ne y\right)\right\}\right|$$
4	2 3	ax-mp	$$⊢D\left(\left\{A\right\}\right)=\left|\left\{f|\left(f:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\wedge \forall y\in \left\{A\right\}f\left(y\right)\ne y\right)\right\}\right|$$
5		f1of	$$⊢f:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\to f:\left\{A\right\}⟶\left\{A\right\}$$
6	5	adantr	$$⊢\left(f:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\wedge \forall y\in \left\{A\right\}f\left(y\right)\ne y\right)\to f:\left\{A\right\}⟶\left\{A\right\}$$
7		snidg	$$⊢A\in V\to A\in \left\{A\right\}$$
8		ffvelcdm	$$⊢\left(f:\left\{A\right\}⟶\left\{A\right\}\wedge A\in \left\{A\right\}\right)\to f\left(A\right)\in \left\{A\right\}$$
9	6 7 8	syl2anr	$$⊢\left(A\in V\wedge \left(f:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\wedge \forall y\in \left\{A\right\}f\left(y\right)\ne y\right)\right)\to f\left(A\right)\in \left\{A\right\}$$
10		simpr	$$⊢\left(f:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\wedge \forall y\in \left\{A\right\}f\left(y\right)\ne y\right)\to \forall y\in \left\{A\right\}f\left(y\right)\ne y$$
11		fveq2	$$⊢y=A\to f\left(y\right)=f\left(A\right)$$
12		id	$$⊢y=A\to y=A$$
13	11 12	neeq12d	$$⊢y=A\to \left(f\left(y\right)\ne y\leftrightarrow f\left(A\right)\ne A\right)$$
14	13	rspcva	$$⊢\left(A\in \left\{A\right\}\wedge \forall y\in \left\{A\right\}f\left(y\right)\ne y\right)\to f\left(A\right)\ne A$$
15	7 10 14	syl2an	$$⊢\left(A\in V\wedge \left(f:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\wedge \forall y\in \left\{A\right\}f\left(y\right)\ne y\right)\right)\to f\left(A\right)\ne A$$
16		nelsn	$$⊢f\left(A\right)\ne A\to \neg f\left(A\right)\in \left\{A\right\}$$
17	15 16	syl	$$⊢\left(A\in V\wedge \left(f:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\wedge \forall y\in \left\{A\right\}f\left(y\right)\ne y\right)\right)\to \neg f\left(A\right)\in \left\{A\right\}$$
18	9 17	pm2.21dd	$$⊢\left(A\in V\wedge \left(f:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\wedge \forall y\in \left\{A\right\}f\left(y\right)\ne y\right)\right)\to f\in \varnothing$$
19	18	ex	$$⊢A\in V\to \left(\left(f:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\wedge \forall y\in \left\{A\right\}f\left(y\right)\ne y\right)\to f\in \varnothing \right)$$
20	19	abssdv	$$⊢A\in V\to \left\{f|\left(f:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\wedge \forall y\in \left\{A\right\}f\left(y\right)\ne y\right)\right\}\subseteq \varnothing$$
21		ss0	$$⊢\left\{f|\left(f:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\wedge \forall y\in \left\{A\right\}f\left(y\right)\ne y\right)\right\}\subseteq \varnothing \to \left\{f|\left(f:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\wedge \forall y\in \left\{A\right\}f\left(y\right)\ne y\right)\right\}=\varnothing$$
22	20 21	syl	$$⊢A\in V\to \left\{f|\left(f:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\wedge \forall y\in \left\{A\right\}f\left(y\right)\ne y\right)\right\}=\varnothing$$
23	22	fveq2d	$$⊢A\in V\to \left|\left\{f|\left(f:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\wedge \forall y\in \left\{A\right\}f\left(y\right)\ne y\right)\right\}\right|=\left|\varnothing \right|$$
24	4 23	eqtrid	$$⊢A\in V\to D\left(\left\{A\right\}\right)=\left|\varnothing \right|$$
25		hash0	$$⊢\left|\varnothing \right|=0$$
26	24 25	eqtrdi	$$⊢A\in V\to D\left(\left\{A\right\}\right)=0$$