Step | Hyp | Ref
| Expression |
1 | | riotaex 7318 |
. . . 4
β’
(β©π¦
β π (π¦πΊπ₯) = (GIdβπΊ)) β V |
2 | | eqid 2733 |
. . . 4
β’ (π₯ β π β¦ (β©π¦ β π (π¦πΊπ₯) = (GIdβπΊ))) = (π₯ β π β¦ (β©π¦ β π (π¦πΊπ₯) = (GIdβπΊ))) |
3 | 1, 2 | fnmpti 6645 |
. . 3
β’ (π₯ β π β¦ (β©π¦ β π (π¦πΊπ₯) = (GIdβπΊ))) Fn π |
4 | | grpasscan1.1 |
. . . . 5
β’ π = ran πΊ |
5 | | eqid 2733 |
. . . . 5
β’
(GIdβπΊ) =
(GIdβπΊ) |
6 | | grpasscan1.2 |
. . . . 5
β’ π = (invβπΊ) |
7 | 4, 5, 6 | grpoinvfval 29506 |
. . . 4
β’ (πΊ β GrpOp β π = (π₯ β π β¦ (β©π¦ β π (π¦πΊπ₯) = (GIdβπΊ)))) |
8 | 7 | fneq1d 6596 |
. . 3
β’ (πΊ β GrpOp β (π Fn π β (π₯ β π β¦ (β©π¦ β π (π¦πΊπ₯) = (GIdβπΊ))) Fn π)) |
9 | 3, 8 | mpbiri 258 |
. 2
β’ (πΊ β GrpOp β π Fn π) |
10 | | fnrnfv 6903 |
. . . 4
β’ (π Fn π β ran π = {π¦ β£ βπ₯ β π π¦ = (πβπ₯)}) |
11 | 9, 10 | syl 17 |
. . 3
β’ (πΊ β GrpOp β ran π = {π¦ β£ βπ₯ β π π¦ = (πβπ₯)}) |
12 | 4, 6 | grpoinvcl 29508 |
. . . . . . 7
β’ ((πΊ β GrpOp β§ π¦ β π) β (πβπ¦) β π) |
13 | 4, 6 | grpo2inv 29515 |
. . . . . . . 8
β’ ((πΊ β GrpOp β§ π¦ β π) β (πβ(πβπ¦)) = π¦) |
14 | 13 | eqcomd 2739 |
. . . . . . 7
β’ ((πΊ β GrpOp β§ π¦ β π) β π¦ = (πβ(πβπ¦))) |
15 | | fveq2 6843 |
. . . . . . . 8
β’ (π₯ = (πβπ¦) β (πβπ₯) = (πβ(πβπ¦))) |
16 | 15 | rspceeqv 3596 |
. . . . . . 7
β’ (((πβπ¦) β π β§ π¦ = (πβ(πβπ¦))) β βπ₯ β π π¦ = (πβπ₯)) |
17 | 12, 14, 16 | syl2anc 585 |
. . . . . 6
β’ ((πΊ β GrpOp β§ π¦ β π) β βπ₯ β π π¦ = (πβπ₯)) |
18 | 17 | ex 414 |
. . . . 5
β’ (πΊ β GrpOp β (π¦ β π β βπ₯ β π π¦ = (πβπ₯))) |
19 | | simpr 486 |
. . . . . . 7
β’ (((πΊ β GrpOp β§ π₯ β π) β§ π¦ = (πβπ₯)) β π¦ = (πβπ₯)) |
20 | 4, 6 | grpoinvcl 29508 |
. . . . . . . 8
β’ ((πΊ β GrpOp β§ π₯ β π) β (πβπ₯) β π) |
21 | 20 | adantr 482 |
. . . . . . 7
β’ (((πΊ β GrpOp β§ π₯ β π) β§ π¦ = (πβπ₯)) β (πβπ₯) β π) |
22 | 19, 21 | eqeltrd 2834 |
. . . . . 6
β’ (((πΊ β GrpOp β§ π₯ β π) β§ π¦ = (πβπ₯)) β π¦ β π) |
23 | 22 | rexlimdva2 3151 |
. . . . 5
β’ (πΊ β GrpOp β
(βπ₯ β π π¦ = (πβπ₯) β π¦ β π)) |
24 | 18, 23 | impbid 211 |
. . . 4
β’ (πΊ β GrpOp β (π¦ β π β βπ₯ β π π¦ = (πβπ₯))) |
25 | 24 | abbi2dv 2868 |
. . 3
β’ (πΊ β GrpOp β π = {π¦ β£ βπ₯ β π π¦ = (πβπ₯)}) |
26 | 11, 25 | eqtr4d 2776 |
. 2
β’ (πΊ β GrpOp β ran π = π) |
27 | | fveq2 6843 |
. . . 4
β’ ((πβπ₯) = (πβπ¦) β (πβ(πβπ₯)) = (πβ(πβπ¦))) |
28 | 4, 6 | grpo2inv 29515 |
. . . . . 6
β’ ((πΊ β GrpOp β§ π₯ β π) β (πβ(πβπ₯)) = π₯) |
29 | 28, 13 | eqeqan12d 2747 |
. . . . 5
β’ (((πΊ β GrpOp β§ π₯ β π) β§ (πΊ β GrpOp β§ π¦ β π)) β ((πβ(πβπ₯)) = (πβ(πβπ¦)) β π₯ = π¦)) |
30 | 29 | anandis 677 |
. . . 4
β’ ((πΊ β GrpOp β§ (π₯ β π β§ π¦ β π)) β ((πβ(πβπ₯)) = (πβ(πβπ¦)) β π₯ = π¦)) |
31 | 27, 30 | imbitrid 243 |
. . 3
β’ ((πΊ β GrpOp β§ (π₯ β π β§ π¦ β π)) β ((πβπ₯) = (πβπ¦) β π₯ = π¦)) |
32 | 31 | ralrimivva 3194 |
. 2
β’ (πΊ β GrpOp β
βπ₯ β π βπ¦ β π ((πβπ₯) = (πβπ¦) β π₯ = π¦)) |
33 | | dff1o6 7222 |
. 2
β’ (π:πβ1-1-ontoβπ β (π Fn π β§ ran π = π β§ βπ₯ β π βπ¦ β π ((πβπ₯) = (πβπ¦) β π₯ = π¦))) |
34 | 9, 26, 32, 33 | syl3anbrc 1344 |
1
β’ (πΊ β GrpOp β π:πβ1-1-ontoβπ) |