Theorem derang0

Description: The derangement number of the empty set. (Contributed by Mario Carneiro, 19-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		derang.d	⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
2		0fin	⊢ ∅ ∈ Fin
3	1	derangval	⊢ ( ∅ ∈ Fin → ( 𝐷 ‘ ∅ ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : ∅ –1-1-onto→ ∅ ∧ ∀ 𝑦 ∈ ∅ ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
4	2 3	ax-mp	⊢ ( 𝐷 ‘ ∅ ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : ∅ –1-1-onto→ ∅ ∧ ∀ 𝑦 ∈ ∅ ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } )
5		ral0	⊢ ∀ 𝑦 ∈ ∅ ( 𝑓 ‘ 𝑦 ) ≠ 𝑦
6	5	biantru	⊢ ( 𝑓 : ∅ –1-1-onto→ ∅ ↔ ( 𝑓 : ∅ –1-1-onto→ ∅ ∧ ∀ 𝑦 ∈ ∅ ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) )
7		eqid	⊢ ∅ = ∅
8		f1o00	⊢ ( 𝑓 : ∅ –1-1-onto→ ∅ ↔ ( 𝑓 = ∅ ∧ ∅ = ∅ ) )
9	7 8	mpbiran2	⊢ ( 𝑓 : ∅ –1-1-onto→ ∅ ↔ 𝑓 = ∅ )
10	6 9	bitr3i	⊢ ( ( 𝑓 : ∅ –1-1-onto→ ∅ ∧ ∀ 𝑦 ∈ ∅ ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) ↔ 𝑓 = ∅ )
11	10	abbii	⊢ { 𝑓 ∣ ( 𝑓 : ∅ –1-1-onto→ ∅ ∧ ∀ 𝑦 ∈ ∅ ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } = { 𝑓 ∣ 𝑓 = ∅ }
12		df-sn	⊢ { ∅ } = { 𝑓 ∣ 𝑓 = ∅ }
13	11 12	eqtr4i	⊢ { 𝑓 ∣ ( 𝑓 : ∅ –1-1-onto→ ∅ ∧ ∀ 𝑦 ∈ ∅ ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } = { ∅ }
14	13	fveq2i	⊢ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : ∅ –1-1-onto→ ∅ ∧ ∀ 𝑦 ∈ ∅ ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) = ( ♯ ‘ { ∅ } )
15		0ex	⊢ ∅ ∈ V
16		hashsng	⊢ ( ∅ ∈ V → ( ♯ ‘ { ∅ } ) = 1 )
17	15 16	ax-mp	⊢ ( ♯ ‘ { ∅ } ) = 1
18	4 14 17	3eqtri	⊢ ( 𝐷 ‘ ∅ ) = 1