Metamath Proof Explorer

Theorem symgextfo

Description: The extension of a permutation, fixing the additional element, is an onto function. (Contributed by AV, 7-Jan-2019)

Ref Expression
Hypotheses symgext.s 
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
symgext.e 
|- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )
Assertion symgextfo 
|- ( ( K e. N /\ Z e. S ) -> E : N -onto-> N )

Proof

Step Hyp Ref Expression
1 symgext.s 
 |-  S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
2 symgext.e 
 |-  E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )
3 1 2 symgextf 
 |-  ( ( K e. N /\ Z e. S ) -> E : N --> N )
4 eqid 
 |-  ( SymGrp ` ( N \ { K } ) ) = ( SymGrp ` ( N \ { K } ) )
5 4 1 symgbasf1o 
 |-  ( Z e. S -> Z : ( N \ { K } ) -1-1-onto-> ( N \ { K } ) )
6 f1ofo 
 |-  ( Z : ( N \ { K } ) -1-1-onto-> ( N \ { K } ) -> Z : ( N \ { K } ) -onto-> ( N \ { K } ) )
7 5 6 syl 
 |-  ( Z e. S -> Z : ( N \ { K } ) -onto-> ( N \ { K } ) )
8 7 adantl 
 |-  ( ( K e. N /\ Z e. S ) -> Z : ( N \ { K } ) -onto-> ( N \ { K } ) )
9 dffo3 
 |-  ( Z : ( N \ { K } ) -onto-> ( N \ { K } ) <-> ( Z : ( N \ { K } ) --> ( N \ { K } ) /\ A. k e. ( N \ { K } ) E. i e. ( N \ { K } ) k = ( Z ` i ) ) )
10 8 9 sylib 
 |-  ( ( K e. N /\ Z e. S ) -> ( Z : ( N \ { K } ) --> ( N \ { K } ) /\ A. k e. ( N \ { K } ) E. i e. ( N \ { K } ) k = ( Z ` i ) ) )
11 10 simprd 
 |-  ( ( K e. N /\ Z e. S ) -> A. k e. ( N \ { K } ) E. i e. ( N \ { K } ) k = ( Z ` i ) )
12 1 2 symgextfv 
 |-  ( ( K e. N /\ Z e. S ) -> ( i e. ( N \ { K } ) -> ( E ` i ) = ( Z ` i ) ) )
13 12 imp 
 |-  ( ( ( K e. N /\ Z e. S ) /\ i e. ( N \ { K } ) ) -> ( E ` i ) = ( Z ` i ) )
14 13 eqeq2d 
 |-  ( ( ( K e. N /\ Z e. S ) /\ i e. ( N \ { K } ) ) -> ( k = ( E ` i ) <-> k = ( Z ` i ) ) )
15 14 rexbidva 
 |-  ( ( K e. N /\ Z e. S ) -> ( E. i e. ( N \ { K } ) k = ( E ` i ) <-> E. i e. ( N \ { K } ) k = ( Z ` i ) ) )
16 15 ralbidv 
 |-  ( ( K e. N /\ Z e. S ) -> ( A. k e. ( N \ { K } ) E. i e. ( N \ { K } ) k = ( E ` i ) <-> A. k e. ( N \ { K } ) E. i e. ( N \ { K } ) k = ( Z ` i ) ) )
17 11 16 mpbird 
 |-  ( ( K e. N /\ Z e. S ) -> A. k e. ( N \ { K } ) E. i e. ( N \ { K } ) k = ( E ` i ) )
18 difssd 
 |-  ( k e. ( N \ { K } ) -> ( N \ { K } ) C_ N )
19 ssrexv 
 |-  ( ( N \ { K } ) C_ N -> ( E. i e. ( N \ { K } ) k = ( E ` i ) -> E. i e. N k = ( E ` i ) ) )
20 18 19 syl 
 |-  ( k e. ( N \ { K } ) -> ( E. i e. ( N \ { K } ) k = ( E ` i ) -> E. i e. N k = ( E ` i ) ) )
21 20 ralimia 
 |-  ( A. k e. ( N \ { K } ) E. i e. ( N \ { K } ) k = ( E ` i ) -> A. k e. ( N \ { K } ) E. i e. N k = ( E ` i ) )
22 17 21 syl 
 |-  ( ( K e. N /\ Z e. S ) -> A. k e. ( N \ { K } ) E. i e. N k = ( E ` i ) )
23 simpl 
 |-  ( ( K e. N /\ Z e. S ) -> K e. N )
24 1 2 symgextfve 
 |-  ( K e. N -> ( i = K -> ( E ` i ) = K ) )
25 24 adantr 
 |-  ( ( K e. N /\ Z e. S ) -> ( i = K -> ( E ` i ) = K ) )
26 25 imp 
 |-  ( ( ( K e. N /\ Z e. S ) /\ i = K ) -> ( E ` i ) = K )
27 26 eqcomd 
 |-  ( ( ( K e. N /\ Z e. S ) /\ i = K ) -> K = ( E ` i ) )
28 23 27 rspcedeq2vd 
 |-  ( ( K e. N /\ Z e. S ) -> E. i e. N K = ( E ` i ) )
29 eqeq1 
 |-  ( k = K -> ( k = ( E ` i ) <-> K = ( E ` i ) ) )
30 29 rexbidv 
 |-  ( k = K -> ( E. i e. N k = ( E ` i ) <-> E. i e. N K = ( E ` i ) ) )
31 30 ralunsn 
 |-  ( K e. N -> ( A. k e. ( ( N \ { K } ) u. { K } ) E. i e. N k = ( E ` i ) <-> ( A. k e. ( N \ { K } ) E. i e. N k = ( E ` i ) /\ E. i e. N K = ( E ` i ) ) ) )
32 31 adantr 
 |-  ( ( K e. N /\ Z e. S ) -> ( A. k e. ( ( N \ { K } ) u. { K } ) E. i e. N k = ( E ` i ) <-> ( A. k e. ( N \ { K } ) E. i e. N k = ( E ` i ) /\ E. i e. N K = ( E ` i ) ) ) )
33 22 28 32 mpbir2and 
 |-  ( ( K e. N /\ Z e. S ) -> A. k e. ( ( N \ { K } ) u. { K } ) E. i e. N k = ( E ` i ) )
34 difsnid 
 |-  ( K e. N -> ( ( N \ { K } ) u. { K } ) = N )
35 34 eqcomd 
 |-  ( K e. N -> N = ( ( N \ { K } ) u. { K } ) )
36 35 raleqdv 
 |-  ( K e. N -> ( A. k e. N E. i e. N k = ( E ` i ) <-> A. k e. ( ( N \ { K } ) u. { K } ) E. i e. N k = ( E ` i ) ) )
37 36 adantr 
 |-  ( ( K e. N /\ Z e. S ) -> ( A. k e. N E. i e. N k = ( E ` i ) <-> A. k e. ( ( N \ { K } ) u. { K } ) E. i e. N k = ( E ` i ) ) )
38 33 37 mpbird 
 |-  ( ( K e. N /\ Z e. S ) -> A. k e. N E. i e. N k = ( E ` i ) )
39 dffo3 
 |-  ( E : N -onto-> N <-> ( E : N --> N /\ A. k e. N E. i e. N k = ( E ` i ) ) )
40 3 38 39 sylanbrc 
 |-  ( ( K e. N /\ Z e. S ) -> E : N -onto-> N )