Theorem deranglem

Description: Lemma for derangements. (Contributed by Mario Carneiro, 19-Jan-2015)

	Ref	Expression
Assertion	deranglem	⊢ ( 𝐴 ∈ Fin → { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝜑 ) } ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		mapfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( 𝐴 ↑m 𝐴 ) ∈ Fin )
2		f1of	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐴 → 𝑓 : 𝐴 ⟶ 𝐴 )
3	2	adantr	⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝜑 ) → 𝑓 : 𝐴 ⟶ 𝐴 )
4		elmapg	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) ↔ 𝑓 : 𝐴 ⟶ 𝐴 ) )
5	3 4	imbitrrid	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝜑 ) → 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) ) )
6	5	abssdv	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ Fin ) → { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝜑 ) } ⊆ ( 𝐴 ↑m 𝐴 ) )
7		ssfi	⊢ ( ( ( 𝐴 ↑m 𝐴 ) ∈ Fin ∧ { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝜑 ) } ⊆ ( 𝐴 ↑m 𝐴 ) ) → { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝜑 ) } ∈ Fin )
8	1 6 7	syl2anc	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ Fin ) → { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝜑 ) } ∈ Fin )
9	8	anidms	⊢ ( 𝐴 ∈ Fin → { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝜑 ) } ∈ Fin )