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	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
	symgfixf.q	⊢ 𝑄 = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
	symgfixf.s	⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
	symgfixf.h	⊢ 𝐻 = ( 𝑞 ∈ 𝑄 ↦ ( 𝑞 ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
Assertion	symgfixf1o	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝐻 : 𝑄 –1-1-onto→ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		symgfixf.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2		symgfixf.q	⊢ 𝑄 = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
3		symgfixf.s	⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
4		symgfixf.h	⊢ 𝐻 = ( 𝑞 ∈ 𝑄 ↦ ( 𝑞 ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
5	1 2 3 4	symgfixf1	⊢ ( 𝐾 ∈ 𝑁 → 𝐻 : 𝑄 –1-1→ 𝑆 )
6	5	adantl	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝐻 : 𝑄 –1-1→ 𝑆 )
7	1 2 3 4	symgfixfo	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝐻 : 𝑄 –onto→ 𝑆 )
8		df-f1o	⊢ ( 𝐻 : 𝑄 –1-1-onto→ 𝑆 ↔ ( 𝐻 : 𝑄 –1-1→ 𝑆 ∧ 𝐻 : 𝑄 –onto→ 𝑆 ) )
9	6 7 8	sylanbrc	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝐻 : 𝑄 –1-1-onto→ 𝑆 )