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	⊢ 𝑃 = ( 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→ 𝑆 )