deranglem

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

		Ref	Expression
	Assertion	deranglem	$⊢ A \in Fin \to \{f \| (f : A \underset{1-1 onto}{⟶} A \land φ)\} \in Fin$

Step	Hyp	Ref	Expression
1		mapfi	$⊢ (A \in Fin \land A \in Fin) \to A^{A} \in Fin$
2		f1of	$⊢ f : A \underset{1-1 onto}{⟶} A \to f : A ⟶ A$
3	2	adantr	$⊢ (f : A \underset{1-1 onto}{⟶} A \land φ) \to f : A ⟶ A$
4		elmapg	$⊢ (A \in Fin \land A \in Fin) \to (f \in (A^{A}) \leftrightarrow f : A ⟶ A)$
5	3 4	imbitrrid	$⊢ (A \in Fin \land A \in Fin) \to ((f : A \underset{1-1 onto}{⟶} A \land φ) \to f \in (A^{A}))$
6	5	abssdv	$⊢ (A \in Fin \land A \in Fin) \to \{f \| (f : A \underset{1-1 onto}{⟶} A \land φ)\} \subseteq A^{A}$
7		ssfi	$⊢ (A^{A} \in Fin \land \{f \| (f : A \underset{1-1 onto}{⟶} A \land φ)\} \subseteq A^{A}) \to \{f \| (f : A \underset{1-1 onto}{⟶} A \land φ)\} \in Fin$
8	1 6 7	syl2anc	$⊢ (A \in Fin \land A \in Fin) \to \{f \| (f : A \underset{1-1 onto}{⟶} A \land φ)\} \in Fin$
9	8	anidms	$⊢ A \in Fin \to \{f \| (f : A \underset{1-1 onto}{⟶} A \land φ)\} \in Fin$

Metamath Proof Explorer