symgfixfolem1

	Ref	Expression
Hypotheses	symgfixf.p	$⊢ P = {Base}_{SymGrp (N)}$
	symgfixf.q	$⊢ Q = \{q \in P \| q (K) = K\}$
	symgfixf.s	$⊢ S = {Base}_{SymGrp (N ∖ \{K\})}$
	symgfixf.h	$⊢ H = (q \in Q ⟼ {q ↾}_{(N ∖ \{K\})})$
	symgfixfo.e	$⊢ E = (x \in N ⟼ if (x = K, K, Z (x)))$
Assertion	symgfixfolem1	$⊢ (N \in V \land K \in N \land Z \in S) \to E \in Q$

Step	Hyp	Ref	Expression
1		symgfixf.p	$⊢ P = {Base}_{SymGrp (N)}$
2		symgfixf.q	$⊢ Q = \{q \in P \| q (K) = K\}$
3		symgfixf.s	$⊢ S = {Base}_{SymGrp (N ∖ \{K\})}$
4		symgfixf.h	$⊢ H = (q \in Q ⟼ {q ↾}_{(N ∖ \{K\})})$
5		symgfixfo.e	$⊢ E = (x \in N ⟼ if (x = K, K, Z (x)))$
6	3 5	symgextf1o	$⊢ (K \in N \land Z \in S) \to E : N \underset{1-1 onto}{⟶} N$
7	6	3adant1	$⊢ (N \in V \land K \in N \land Z \in S) \to E : N \underset{1-1 onto}{⟶} N$
8		iftrue	$⊢ x = K \to if (x = K, K, Z (x)) = K$
9		simp2	$⊢ (N \in V \land K \in N \land Z \in S) \to K \in N$
10	5 8 9 9	fvmptd3	$⊢ (N \in V \land K \in N \land Z \in S) \to E (K) = K$
11		mptexg	$⊢ N \in V \to (x \in N ⟼ if (x = K, K, Z (x))) \in V$
12	11	3ad2ant1	$⊢ (N \in V \land K \in N \land Z \in S) \to (x \in N ⟼ if (x = K, K, Z (x))) \in V$
13	5 12	eqeltrid	$⊢ (N \in V \land K \in N \land Z \in S) \to E \in V$
14	1 2	symgfixelq	$⊢ E \in V \to (E \in Q \leftrightarrow (E : N \underset{1-1 onto}{⟶} N \land E (K) = K))$
15	13 14	syl	$⊢ (N \in V \land K \in N \land Z \in S) \to (E \in Q \leftrightarrow (E : N \underset{1-1 onto}{⟶} N \land E (K) = K))$
16	7 10 15	mpbir2and	$⊢ (N \in V \land K \in N \land Z \in S) \to E \in Q$

Metamath Proof Explorer