| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Mapping of the inverse function of a group. |
| Ref | Expression |
|---|---|
| grpasscan1.1 |
|
| grpasscan1.2 |
|
| Ref | Expression |
|---|---|
| grpinvf |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rnexg 3419 |
. . . . . . . . . 10
| |
| 2 | grpasscan1.1 |
. . . . . . . . . 10
| |
| 3 | 1, 2 | syl5eqel 1589 |
. . . . . . . . 9
|
| 4 | rabexg 2775 |
. . . . . . . . 9
| |
| 5 | 3, 4 | syl 10 |
. . . . . . . 8
|
| 6 | uniexg 2925 |
. . . . . . . 8
| |
| 7 | 5, 6 | syl 10 |
. . . . . . 7
|
| 8 | 7 | adantr 389 |
. . . . . 6
|
| 9 | 8 | r19.21aiva 1752 |
. . . . 5
|
| 10 | eqid 1512 |
. . . . . 6
| |
| 11 | 10 | fnopab2g 3691 |
. . . . 5
|
| 12 | 9, 11 | sylib 196 |
. . . 4
|
| 13 | eqid 1512 |
. . . . . 6
| |
| 14 | grpasscan1.2 |
. . . . . 6
| |
| 15 | 2, 13, 14 | grpinvfval 8185 |
. . . . 5
|
| 16 | fneq1 3657 |
. . . . 5
| |
| 17 | 15, 16 | syl 10 |
. . . 4
|
| 18 | 12, 17 | mpbird 194 |
. . 3
|
| 19 | fnrnfv 3835 |
. . . . 5
| |
| 20 | 18, 19 | syl 10 |
. . . 4
|
| 21 | fveq2 3800 |
. . . . . . . . . 10
| |
| 22 | 21 | eqeq2d 1523 |
. . . . . . . . 9
|
| 23 | 22 | rcla4ev 1915 |
. . . . . . . 8
|
| 24 | 2, 14 | grpinvcl 8187 |
. . . . . . . 8
|
| 25 | 2, 14 | grp2inv 8197 |
. . . . . . . . 9
|
| 26 | 25 | eqcomd 1517 |
. . . . . . . 8
|
| 27 | 23, 24, 26 | sylanc 473 |
. . . . . . 7
|
| 28 | 27 | ex 371 |
. . . . . 6
|
| 29 | pm3.27 321 |
. . . . . . . . 9
| |
| 30 | 2, 14 | grpinvcl 8187 |
. . . . . . . . . 10
|
| 31 | 30 | adantr 389 |
. . . . . . . . 9
|
| 32 | 29, 31 | eqeltrd 1585 |
. . . . . . . 8
|
| 33 | 32 | exp31 376 |
. . . . . . 7
|
| 34 | 33 | r19.23adv 1784 |
. . . . . 6
|
| 35 | 28, 34 | impbid 518 |
. . . . 5
|
| 36 | 35 | abbi2dv 1615 |
. . . 4
|
| 37 | 20, 36 | eqtr4d 1547 |
. . 3
|
| 38 | 2, 14 | grp2inv 8197 |
. . . . . . . 8
|
| 39 | 38, 25 | eqeqan12d 1527 |
. . . . . . 7
|
| 40 | 39 | anandis 514 |
. . . . . 6
|
| 41 | fveq2 3800 |
. . . . . 6
| |
| 42 | 40, 41 | syl5bi 206 |
. . . . 5
|
| 43 | 42 | ex 371 |
. . . 4
|
| 44 | 43 | r19.21aivv 1758 |
. . 3
|
| 45 | 18, 37, 44 | 3jca 822 |
. 2
|
| 46 | dff1o6 3953 |
. 2
| |
| 47 | 45, 46 | sylibr 198 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: invfval 8380 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 994 ax-gen 995 ax-8 996 ax-9 997 ax-10 998 ax-11 999 ax-12 1000 ax-13 1001 ax-14 1002 ax-17 1003 ax-4 1005 ax-5o 1007 ax-6o 1010 ax-9o 1155 ax-10o 1173 ax-16 1243 ax-11o 1251 ax-ext 1494 ax-rep 2744 ax-sep 2754 ax-pow 2794 ax-pr 2832 ax-un 2920 |
| This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3an 780 df-ex 1013 df-sb 1205 df-eu 1415 df-mo 1416 df-clab 1500 df-cleq 1505 df-clel 1508 df-ne 1624 df-ral 1687 df-rex 1688 df-reu 1689 df-rab 1690 df-v 1850 df-sbc 1979 df-dif 2093 df-un 2094 df-in 2095 df-ss 2097 df-nul 2325 df-pw 2447 df-sn 2457 df-pr 2458 df-op 2461 df-uni 2552 df-br 2670 df-opab 2718 df-id 2889 df-xp 3239 df-rel 3240 df-cnv 3241 df-co 3242 df-dm 3243 df-rn 3244 df-res 3245 df-ima 3246 df-fun 3247 df-fn 3248 df-f 3249 df-f1 3250 df-fo 3251 df-f1o 3252 df-fv 3253 df-opr 4041 df-grp 8157 df-gid 8158 df-ginv 8159 |