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

Metamath Proof Explorer

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→ 𝐷 ) )