Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  symgextfo Structured version   Unicode version

Theorem symgextfo 16573
 Description: The extension of a permutation, fixing the additional element, is an onto function. (Contributed by AV, 7-Jan-2019.)
Hypotheses
Ref Expression
symgext.s
symgext.e
Assertion
Ref Expression
symgextfo
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem symgextfo
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 symgext.s . . 3
2 symgext.e . . 3
31, 2symgextf 16568 . 2
4 eqid 2457 . . . . . . . . . . 11
54, 1symgbasf1o 16534 . . . . . . . . . 10
6 f1ofo 5829 . . . . . . . . . 10
75, 6syl 16 . . . . . . . . 9
87adantl 466 . . . . . . . 8
9 dffo3 6047 . . . . . . . 8
108, 9sylib 196 . . . . . . 7
1110simprd 463 . . . . . 6
121, 2symgextfv 16569 . . . . . . . . . 10
1312imp 429 . . . . . . . . 9
1413eqeq2d 2471 . . . . . . . 8
1514rexbidva 2965 . . . . . . 7
1615ralbidv 2896 . . . . . 6
1711, 16mpbird 232 . . . . 5
18 difssd 3628 . . . . . . 7
19 ssrexv 3561 . . . . . . 7
2018, 19syl 16 . . . . . 6
2120ralimia 2848 . . . . 5
2217, 21syl 16 . . . 4
23 simpl 457 . . . . 5
241, 2symgextfve 16570 . . . . . . . 8
2524adantr 465 . . . . . . 7
2625imp 429 . . . . . 6
2726eqcomd 2465 . . . . 5
2823, 27rspcedeq2vd 3217 . . . 4
29 eqeq1 2461 . . . . . . 7
3029rexbidv 2968 . . . . . 6
3130ralunsn 4239 . . . . 5
3231adantr 465 . . . 4
3322, 28, 32mpbir2and 922 . . 3
34 difsnid 4178 . . . . . 6
3534eqcomd 2465 . . . . 5
3635raleqdv 3060 . . . 4