Theorem derangen

Description: The derangement number is a cardinal invariant, i.e. it only depends on the size of a set and not on its contents. (Contributed by Mario Carneiro, 22-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		derang.d	⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
2	1	derangenlem	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → ( 𝐷 ‘ 𝐴 ) ≤ ( 𝐷 ‘ 𝐵 ) )
3		ensym	⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴 )
4	3	adantr	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → 𝐵 ≈ 𝐴 )
5		enfi	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) )
6	5	biimpar	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → 𝐴 ∈ Fin )
7	1	derangenlem	⊢ ( ( 𝐵 ≈ 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐷 ‘ 𝐵 ) ≤ ( 𝐷 ‘ 𝐴 ) )
8	4 6 7	syl2anc	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → ( 𝐷 ‘ 𝐵 ) ≤ ( 𝐷 ‘ 𝐴 ) )
9	1	derangf	⊢ 𝐷 : Fin ⟶ ℕ0
10	9	ffvelcdmi	⊢ ( 𝐴 ∈ Fin → ( 𝐷 ‘ 𝐴 ) ∈ ℕ0 )
11	6 10	syl	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → ( 𝐷 ‘ 𝐴 ) ∈ ℕ0 )
12	9	ffvelcdmi	⊢ ( 𝐵 ∈ Fin → ( 𝐷 ‘ 𝐵 ) ∈ ℕ0 )
13	12	adantl	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → ( 𝐷 ‘ 𝐵 ) ∈ ℕ0 )
14		nn0re	⊢ ( ( 𝐷 ‘ 𝐴 ) ∈ ℕ0 → ( 𝐷 ‘ 𝐴 ) ∈ ℝ )
15		nn0re	⊢ ( ( 𝐷 ‘ 𝐵 ) ∈ ℕ0 → ( 𝐷 ‘ 𝐵 ) ∈ ℝ )
16		letri3	⊢ ( ( ( 𝐷 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝐷 ‘ 𝐵 ) ∈ ℝ ) → ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝐵 ) ↔ ( ( 𝐷 ‘ 𝐴 ) ≤ ( 𝐷 ‘ 𝐵 ) ∧ ( 𝐷 ‘ 𝐵 ) ≤ ( 𝐷 ‘ 𝐴 ) ) ) )
17	14 15 16	syl2an	⊢ ( ( ( 𝐷 ‘ 𝐴 ) ∈ ℕ0 ∧ ( 𝐷 ‘ 𝐵 ) ∈ ℕ0 ) → ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝐵 ) ↔ ( ( 𝐷 ‘ 𝐴 ) ≤ ( 𝐷 ‘ 𝐵 ) ∧ ( 𝐷 ‘ 𝐵 ) ≤ ( 𝐷 ‘ 𝐴 ) ) ) )
18	11 13 17	syl2anc	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝐵 ) ↔ ( ( 𝐷 ‘ 𝐴 ) ≤ ( 𝐷 ‘ 𝐵 ) ∧ ( 𝐷 ‘ 𝐵 ) ≤ ( 𝐷 ‘ 𝐴 ) ) ) )
19	2 8 18	mpbir2and	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝐵 ) )