This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem symgfixf1o

Description: The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is a bijection. (Contributed by AV, 7-Jan-2019)

		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\})})$
	Assertion	symgfixf1o	$⊢ (N \in V \land K \in N) \to H : Q \underset{1-1 onto}{⟶} S$

Proof

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	1 2 3 4	symgfixf1	$⊢ K \in N \to H : Q \underset{1-1}{⟶} S$
6	5	adantl	$⊢ (N \in V \land K \in N) \to H : Q \underset{1-1}{⟶} S$
7	1 2 3 4	symgfixfo	$⊢ (N \in V \land K \in N) \to H : Q \underset{onto}{⟶} S$
8		df-f1o	$⊢ H : Q \underset{1-1 onto}{⟶} S \leftrightarrow (H : Q \underset{1-1}{⟶} S \land H : Q \underset{onto}{⟶} S)$
9	6 7 8	sylanbrc	$⊢ (N \in V \land K \in N) \to H : Q \underset{1-1 onto}{⟶} S$