symgextf

Description: The extension of a permutation, fixing the additional element, is a function. (Contributed by AV, 6-Jan-2019)

Step	Hyp	Ref	Expression
1		symgext.s	$⊢ S = {Base}_{SymGrp (N ∖ \{K\})}$
2		symgext.e	$⊢ E = (x \in N ⟼ if (x = K, K, Z (x)))$
3		simplll	$⊢ (((K \in N \land Z \in S) \land x \in N) \land x = K) \to K \in N$
4		simpllr	$⊢ (((K \in N \land Z \in S) \land x \in N) \land \neg x = K) \to Z \in S$
5		simpr	$⊢ ((K \in N \land Z \in S) \land x \in N) \to x \in N$
6		neqne	$⊢ \neg x = K \to x \neq K$
7	5 6	anim12i	$⊢ (((K \in N \land Z \in S) \land x \in N) \land \neg x = K) \to (x \in N \land x \neq K)$
8		eldifsn	$⊢ x \in (N ∖ \{K\}) \leftrightarrow (x \in N \land x \neq K)$
9	7 8	sylibr	$⊢ (((K \in N \land Z \in S) \land x \in N) \land \neg x = K) \to x \in (N ∖ \{K\})$
10		eqid	$⊢ SymGrp (N ∖ \{K\}) = SymGrp (N ∖ \{K\})$
11	10 1	symgfv	$⊢ (Z \in S \land x \in (N ∖ \{K\})) \to Z (x) \in (N ∖ \{K\})$
12	4 9 11	syl2anc	$⊢ (((K \in N \land Z \in S) \land x \in N) \land \neg x = K) \to Z (x) \in (N ∖ \{K\})$
13	12	eldifad	$⊢ (((K \in N \land Z \in S) \land x \in N) \land \neg x = K) \to Z (x) \in N$
14	3 13	ifclda	$⊢ ((K \in N \land Z \in S) \land x \in N) \to if (x = K, K, Z (x)) \in N$
15	14 2	fmptd	$⊢ (K \in N \land Z \in S) \to E : N ⟶ N$

Metamath Proof Explorer