symgfixelq

Description: A permutation of a set fixing an element of the set. (Contributed by AV, 4-Jan-2019)

	Ref	Expression
Hypotheses	symgfixf.p	$⊢ P = {Base}_{SymGrp (N)}$
	symgfixf.q	$⊢ Q = \{q \in P \| q (K) = K\}$
Assertion	symgfixelq	$⊢ F \in V \to (F \in Q \leftrightarrow (F : N \underset{1-1 onto}{⟶} N \land F (K) = K))$

Step	Hyp	Ref	Expression
1		symgfixf.p	$⊢ P = {Base}_{SymGrp (N)}$
2		symgfixf.q	$⊢ Q = \{q \in P \| q (K) = K\}$
3		fveq1	$⊢ f = F \to f (K) = F (K)$
4	3	eqeq1d	$⊢ f = F \to (f (K) = K \leftrightarrow F (K) = K)$
5		fveq1	$⊢ q = f \to q (K) = f (K)$
6	5	eqeq1d	$⊢ q = f \to (q (K) = K \leftrightarrow f (K) = K)$
7	6	cbvrabv	$⊢ \{q \in P \| q (K) = K\} = \{f \in P \| f (K) = K\}$
8	2 7	eqtri	$⊢ Q = \{f \in P \| f (K) = K\}$
9	4 8	elrab2	$⊢ F \in Q \leftrightarrow (F \in P \land F (K) = K)$
10		eqid	$⊢ SymGrp (N) = SymGrp (N)$
11	10 1	elsymgbas2	$⊢ F \in V \to (F \in P \leftrightarrow F : N \underset{1-1 onto}{⟶} N)$
12	11	anbi1d	$⊢ F \in V \to ((F \in P \land F (K) = K) \leftrightarrow (F : N \underset{1-1 onto}{⟶} N \land F (K) = K))$
13	9 12	bitrid	$⊢ F \in V \to (F \in Q \leftrightarrow (F : N \underset{1-1 onto}{⟶} N \land F (K) = K))$

Metamath Proof Explorer