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𝑆 )