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 ⊢ P = Base SymGrp ⁡ N
symgfixf.q ⊢ Q = q ∈ P | q ⁡ K = K
symgfixf.s ⊢ S = Base SymGrp ⁡ N ∖ K
symgfixf.d ⊢ D = N ∖ K
Assertion symgfixels ⊢ F ∈ V → F ↾ D ∈ S ↔ F ↾ D : D ⟶ 1-1 onto D

Proof

Step Hyp Ref Expression
1 symgfixf.p ⊢ P = Base SymGrp ⁡ N
2 symgfixf.q ⊢ Q = q ∈ P | q ⁡ K = K
3 symgfixf.s ⊢ S = Base SymGrp ⁡ N ∖ K
4 symgfixf.d ⊢ D = N ∖ K
5 3 eleq2i ⊢ F ↾ D ∈ S ↔ F ↾ D ∈ Base SymGrp ⁡ N ∖ K
6 5 a1i ⊢ F ∈ V → F ↾ D ∈ S ↔ F ↾ D ∈ Base SymGrp ⁡ N ∖ K
7 resexg ⊢ F ∈ V → F ↾ D ∈ V
8 eqid ⊢ SymGrp ⁡ N ∖ K = SymGrp ⁡ N ∖ K
9 eqid ⊢ Base SymGrp ⁡ N ∖ K = Base SymGrp ⁡ N ∖ K
10 8 9 elsymgbas2 ⊢ F ↾ D ∈ V → F ↾ D ∈ Base SymGrp ⁡ N ∖ K ↔ F ↾ D : N ∖ K ⟶ 1-1 onto N ∖ K
11 7 10 syl ⊢ F ∈ V → F ↾ D ∈ Base SymGrp ⁡ N ∖ K ↔ F ↾ D : N ∖ K ⟶ 1-1 onto N ∖ K
12 eqidd ⊢ F ∈ V → F ↾ D = F ↾ D
13 4 a1i ⊢ F ∈ V → D = N ∖ K
14 13 eqcomd ⊢ F ∈ V → N ∖ K = D
15 12 14 14 f1oeq123d ⊢ F ∈ V → F ↾ D : N ∖ K ⟶ 1-1 onto N ∖ K ↔ F ↾ D : D ⟶ 1-1 onto D
16 6 11 15 3bitrd ⊢ F ∈ V → F ↾ D ∈ S ↔ F ↾ D : D ⟶ 1-1 onto D