symgextfo

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

	Ref	Expression
Hypotheses	symgext.s	$⊢ S = {Base}_{SymGrp (N ∖ \{K\})}$
	symgext.e	$⊢ E = (x \in N ⟼ if (x = K, K, Z (x)))$
Assertion	symgextfo	$⊢ (K \in N \land Z \in S) \to E : N \underset{onto}{⟶} N$

Proof

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	1 2	symgextf	$⊢ (K \in N \land Z \in S) \to E : N ⟶ N$
4		eqid	$⊢ SymGrp (N ∖ \{K\}) = SymGrp (N ∖ \{K\})$
5	4 1	symgbasf1o	$⊢ Z \in S \to Z : N ∖ \{K\} \underset{1-1 onto}{⟶} N ∖ \{K\}$
6		f1ofo	$⊢ Z : N ∖ \{K\} \underset{1-1 onto}{⟶} N ∖ \{K\} \to Z : N ∖ \{K\} \underset{onto}{⟶} N ∖ \{K\}$
7	5 6	syl	$⊢ Z \in S \to Z : N ∖ \{K\} \underset{onto}{⟶} N ∖ \{K\}$
8	7	adantl	$⊢ (K \in N \land Z \in S) \to Z : N ∖ \{K\} \underset{onto}{⟶} N ∖ \{K\}$
9		dffo3	$⊢ Z : N ∖ \{K\} \underset{onto}{⟶} N ∖ \{K\} \leftrightarrow (Z : N ∖ \{K\} ⟶ N ∖ \{K\} \land \forall k \in (N ∖ \{K\}) \exists i \in (N ∖ \{K\}) k = Z (i))$
10	8 9	sylib	$⊢ (K \in N \land Z \in S) \to (Z : N ∖ \{K\} ⟶ N ∖ \{K\} \land \forall k \in (N ∖ \{K\}) \exists i \in (N ∖ \{K\}) k = Z (i))$
11	10	simprd	$⊢ (K \in N \land Z \in S) \to \forall k \in (N ∖ \{K\}) \exists i \in (N ∖ \{K\}) k = Z (i)$
12	1 2	symgextfv	$⊢ (K \in N \land Z \in S) \to (i \in (N ∖ \{K\}) \to E (i) = Z (i))$
13	12	imp	$⊢ ((K \in N \land Z \in S) \land i \in (N ∖ \{K\})) \to E (i) = Z (i)$
14	13	eqeq2d	$⊢ ((K \in N \land Z \in S) \land i \in (N ∖ \{K\})) \to (k = E (i) \leftrightarrow k = Z (i))$
15	14	rexbidva	$⊢ (K \in N \land Z \in S) \to (\exists i \in (N ∖ \{K\}) k = E (i) \leftrightarrow \exists i \in (N ∖ \{K\}) k = Z (i))$
16	15	ralbidv	$⊢ (K \in N \land Z \in S) \to (\forall k \in (N ∖ \{K\}) \exists i \in (N ∖ \{K\}) k = E (i) \leftrightarrow \forall k \in (N ∖ \{K\}) \exists i \in (N ∖ \{K\}) k = Z (i))$
17	11 16	mpbird	$⊢ (K \in N \land Z \in S) \to \forall k \in (N ∖ \{K\}) \exists i \in (N ∖ \{K\}) k = E (i)$
18		difssd	$⊢ k \in (N ∖ \{K\}) \to N ∖ \{K\} \subseteq N$
19		ssrexv	$⊢ N ∖ \{K\} \subseteq N \to (\exists i \in (N ∖ \{K\}) k = E (i) \to \exists i \in N k = E (i))$
20	18 19	syl	$⊢ k \in (N ∖ \{K\}) \to (\exists i \in (N ∖ \{K\}) k = E (i) \to \exists i \in N k = E (i))$
21	20	ralimia	$⊢ \forall k \in (N ∖ \{K\}) \exists i \in (N ∖ \{K\}) k = E (i) \to \forall k \in (N ∖ \{K\}) \exists i \in N k = E (i)$
22	17 21	syl	$⊢ (K \in N \land Z \in S) \to \forall k \in (N ∖ \{K\}) \exists i \in N k = E (i)$
23		simpl	$⊢ (K \in N \land Z \in S) \to K \in N$
24	1 2	symgextfve	$⊢ K \in N \to (i = K \to E (i) = K)$
25	24	adantr	$⊢ (K \in N \land Z \in S) \to (i = K \to E (i) = K)$
26	25	imp	$⊢ ((K \in N \land Z \in S) \land i = K) \to E (i) = K$
27	26	eqcomd	$⊢ ((K \in N \land Z \in S) \land i = K) \to K = E (i)$
28	23 27	rspcedeqvd	$⊢ (K \in N \land Z \in S) \to \exists i \in N K = E (i)$
29		eqeq1	$⊢ k = K \to (k = E (i) \leftrightarrow K = E (i))$
30	29	rexbidv	$⊢ k = K \to (\exists i \in N k = E (i) \leftrightarrow \exists i \in N K = E (i))$
31	30	ralunsn	$⊢ K \in N \to (\forall k \in ((N ∖ \{K\}) \cup \{K\}) \exists i \in N k = E (i) \leftrightarrow (\forall k \in (N ∖ \{K\}) \exists i \in N k = E (i) \land \exists i \in N K = E (i)))$
32	31	adantr	$⊢ (K \in N \land Z \in S) \to (\forall k \in ((N ∖ \{K\}) \cup \{K\}) \exists i \in N k = E (i) \leftrightarrow (\forall k \in (N ∖ \{K\}) \exists i \in N k = E (i) \land \exists i \in N K = E (i)))$
33	22 28 32	mpbir2and	$⊢ (K \in N \land Z \in S) \to \forall k \in ((N ∖ \{K\}) \cup \{K\}) \exists i \in N k = E (i)$
34		difsnid	$⊢ K \in N \to (N ∖ \{K\}) \cup \{K\} = N$
35	34	eqcomd	$⊢ K \in N \to N = (N ∖ \{K\}) \cup \{K\}$
36	35	raleqdv	$⊢ K \in N \to (\forall k \in N \exists i \in N k = E (i) \leftrightarrow \forall k \in ((N ∖ \{K\}) \cup \{K\}) \exists i \in N k = E (i))$
37	36	adantr	$⊢ (K \in N \land Z \in S) \to (\forall k \in N \exists i \in N k = E (i) \leftrightarrow \forall k \in ((N ∖ \{K\}) \cup \{K\}) \exists i \in N k = E (i))$
38	33 37	mpbird	$⊢ (K \in N \land Z \in S) \to \forall k \in N \exists i \in N k = E (i)$
39		dffo3	$⊢ E : N \underset{onto}{⟶} N \leftrightarrow (E : N ⟶ N \land \forall k \in N \exists i \in N k = E (i))$
40	3 38 39	sylanbrc	$⊢ (K \in N \land Z \in S) \to E : N \underset{onto}{⟶} N$

Metamath Proof Explorer

Theorem symgextfo

Proof