Theorem derangsn

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

	Ref	Expression
Hypothesis	derang.d	⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
Assertion	derangsn	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐷 ‘ { 𝐴 } ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		derang.d	⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
2		snfi	⊢ { 𝐴 } ∈ Fin
3	1	derangval	⊢ ( { 𝐴 } ∈ Fin → ( 𝐷 ‘ { 𝐴 } ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
4	2 3	ax-mp	⊢ ( 𝐷 ‘ { 𝐴 } ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } )
5		f1of	⊢ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } → 𝑓 : { 𝐴 } ⟶ { 𝐴 } )
6	5	adantr	⊢ ( ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) → 𝑓 : { 𝐴 } ⟶ { 𝐴 } )
7		snidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
8		ffvelrn	⊢ ( ( 𝑓 : { 𝐴 } ⟶ { 𝐴 } ∧ 𝐴 ∈ { 𝐴 } ) → ( 𝑓 ‘ 𝐴 ) ∈ { 𝐴 } )
9	6 7 8	syl2anr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) ) → ( 𝑓 ‘ 𝐴 ) ∈ { 𝐴 } )
10		simpr	⊢ ( ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) → ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 )
11		fveq2	⊢ ( 𝑦 = 𝐴 → ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝐴 ) )
12		id	⊢ ( 𝑦 = 𝐴 → 𝑦 = 𝐴 )
13	11 12	neeq12d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ( 𝑓 ‘ 𝐴 ) ≠ 𝐴 ) )
14	13	rspcva	⊢ ( ( 𝐴 ∈ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) → ( 𝑓 ‘ 𝐴 ) ≠ 𝐴 )
15	7 10 14	syl2an	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) ) → ( 𝑓 ‘ 𝐴 ) ≠ 𝐴 )
16		nelsn	⊢ ( ( 𝑓 ‘ 𝐴 ) ≠ 𝐴 → ¬ ( 𝑓 ‘ 𝐴 ) ∈ { 𝐴 } )
17	15 16	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) ) → ¬ ( 𝑓 ‘ 𝐴 ) ∈ { 𝐴 } )
18	9 17	pm2.21dd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) ) → 𝑓 ∈ ∅ )
19	18	ex	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) → 𝑓 ∈ ∅ ) )
20	19	abssdv	⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ⊆ ∅ )
21		ss0	⊢ ( { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ⊆ ∅ → { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } = ∅ )
22	20 21	syl	⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } = ∅ )
23	22	fveq2d	⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) = ( ♯ ‘ ∅ ) )
24	4 23	eqtrid	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐷 ‘ { 𝐴 } ) = ( ♯ ‘ ∅ ) )
25		hash0	⊢ ( ♯ ‘ ∅ ) = 0
26	24 25	eqtrdi	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐷 ‘ { 𝐴 } ) = 0 )