Theorem symgfixels

Description: The restriction of a permutation to a set with one element removed is an element of the restricted symmetric group if the restriction is a 1-1 onto function. (Contributed by AV, 4-Jan-2019)

	Ref	Expression
Hypotheses	symgfixf.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
	symgfixf.q	⊢ 𝑄 = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
	symgfixf.s	⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
	symgfixf.d	⊢ 𝐷 = ( 𝑁 ∖ { 𝐾 } )
Assertion	symgfixels	⊢ ( 𝐹 ∈ 𝑉 → ( ( 𝐹 ↾ 𝐷 ) ∈ 𝑆 ↔ ( 𝐹 ↾ 𝐷 ) : 𝐷 –1-1-onto→ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		symgfixf.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2		symgfixf.q	⊢ 𝑄 = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
3		symgfixf.s	⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
4		symgfixf.d	⊢ 𝐷 = ( 𝑁 ∖ { 𝐾 } )
5	3	eleq2i	⊢ ( ( 𝐹 ↾ 𝐷 ) ∈ 𝑆 ↔ ( 𝐹 ↾ 𝐷 ) ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) )
6	5	a1i	⊢ ( 𝐹 ∈ 𝑉 → ( ( 𝐹 ↾ 𝐷 ) ∈ 𝑆 ↔ ( 𝐹 ↾ 𝐷 ) ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ) )
7		resexg	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ↾ 𝐷 ) ∈ V )
8		eqid	⊢ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) )
9		eqid	⊢ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
10	8 9	elsymgbas2	⊢ ( ( 𝐹 ↾ 𝐷 ) ∈ V → ( ( 𝐹 ↾ 𝐷 ) ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ↔ ( 𝐹 ↾ 𝐷 ) : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝑁 ∖ { 𝐾 } ) ) )
11	7 10	syl	⊢ ( 𝐹 ∈ 𝑉 → ( ( 𝐹 ↾ 𝐷 ) ∈ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ↔ ( 𝐹 ↾ 𝐷 ) : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝑁 ∖ { 𝐾 } ) ) )
12		eqidd	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ↾ 𝐷 ) = ( 𝐹 ↾ 𝐷 ) )
13	4	a1i	⊢ ( 𝐹 ∈ 𝑉 → 𝐷 = ( 𝑁 ∖ { 𝐾 } ) )
14	13	eqcomd	⊢ ( 𝐹 ∈ 𝑉 → ( 𝑁 ∖ { 𝐾 } ) = 𝐷 )
15	12 14 14	f1oeq123d	⊢ ( 𝐹 ∈ 𝑉 → ( ( 𝐹 ↾ 𝐷 ) : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝑁 ∖ { 𝐾 } ) ↔ ( 𝐹 ↾ 𝐷 ) : 𝐷 –1-1-onto→ 𝐷 ) )
16	6 11 15	3bitrd	⊢ ( 𝐹 ∈ 𝑉 → ( ( 𝐹 ↾ 𝐷 ) ∈ 𝑆 ↔ ( 𝐹 ↾ 𝐷 ) : 𝐷 –1-1-onto→ 𝐷 ) )