Step | Hyp | Ref
| Expression |
1 | | riotaex 6615 |
. . . 4
⊢
(℩𝑦
∈ 𝑋 (𝑦𝐺𝑥) = (GId‘𝐺)) ∈ V |
2 | | eqid 2622 |
. . . 4
⊢ (𝑥 ∈ 𝑋 ↦ (℩𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = (GId‘𝐺))) = (𝑥 ∈ 𝑋 ↦ (℩𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = (GId‘𝐺))) |
3 | 1, 2 | fnmpti 6022 |
. . 3
⊢ (𝑥 ∈ 𝑋 ↦ (℩𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = (GId‘𝐺))) Fn 𝑋 |
4 | | grpasscan1.1 |
. . . . 5
⊢ 𝑋 = ran 𝐺 |
5 | | eqid 2622 |
. . . . 5
⊢
(GId‘𝐺) =
(GId‘𝐺) |
6 | | grpasscan1.2 |
. . . . 5
⊢ 𝑁 = (inv‘𝐺) |
7 | 4, 5, 6 | grpoinvfval 27376 |
. . . 4
⊢ (𝐺 ∈ GrpOp → 𝑁 = (𝑥 ∈ 𝑋 ↦ (℩𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = (GId‘𝐺)))) |
8 | 7 | fneq1d 5981 |
. . 3
⊢ (𝐺 ∈ GrpOp → (𝑁 Fn 𝑋 ↔ (𝑥 ∈ 𝑋 ↦ (℩𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = (GId‘𝐺))) Fn 𝑋)) |
9 | 3, 8 | mpbiri 248 |
. 2
⊢ (𝐺 ∈ GrpOp → 𝑁 Fn 𝑋) |
10 | | fnrnfv 6242 |
. . . 4
⊢ (𝑁 Fn 𝑋 → ran 𝑁 = {𝑦 ∣ ∃𝑥 ∈ 𝑋 𝑦 = (𝑁‘𝑥)}) |
11 | 9, 10 | syl 17 |
. . 3
⊢ (𝐺 ∈ GrpOp → ran 𝑁 = {𝑦 ∣ ∃𝑥 ∈ 𝑋 𝑦 = (𝑁‘𝑥)}) |
12 | 4, 6 | grpoinvcl 27378 |
. . . . . . 7
⊢ ((𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ 𝑋) |
13 | 4, 6 | grpo2inv 27385 |
. . . . . . . 8
⊢ ((𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋) → (𝑁‘(𝑁‘𝑦)) = 𝑦) |
14 | 13 | eqcomd 2628 |
. . . . . . 7
⊢ ((𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋) → 𝑦 = (𝑁‘(𝑁‘𝑦))) |
15 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑥 = (𝑁‘𝑦) → (𝑁‘𝑥) = (𝑁‘(𝑁‘𝑦))) |
16 | 15 | eqeq2d 2632 |
. . . . . . . 8
⊢ (𝑥 = (𝑁‘𝑦) → (𝑦 = (𝑁‘𝑥) ↔ 𝑦 = (𝑁‘(𝑁‘𝑦)))) |
17 | 16 | rspcev 3309 |
. . . . . . 7
⊢ (((𝑁‘𝑦) ∈ 𝑋 ∧ 𝑦 = (𝑁‘(𝑁‘𝑦))) → ∃𝑥 ∈ 𝑋 𝑦 = (𝑁‘𝑥)) |
18 | 12, 14, 17 | syl2anc 693 |
. . . . . 6
⊢ ((𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋) → ∃𝑥 ∈ 𝑋 𝑦 = (𝑁‘𝑥)) |
19 | 18 | ex 450 |
. . . . 5
⊢ (𝐺 ∈ GrpOp → (𝑦 ∈ 𝑋 → ∃𝑥 ∈ 𝑋 𝑦 = (𝑁‘𝑥))) |
20 | | simpr 477 |
. . . . . . . 8
⊢ (((𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 = (𝑁‘𝑥)) → 𝑦 = (𝑁‘𝑥)) |
21 | 4, 6 | grpoinvcl 27378 |
. . . . . . . . 9
⊢ ((𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋) → (𝑁‘𝑥) ∈ 𝑋) |
22 | 21 | adantr 481 |
. . . . . . . 8
⊢ (((𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 = (𝑁‘𝑥)) → (𝑁‘𝑥) ∈ 𝑋) |
23 | 20, 22 | eqeltrd 2701 |
. . . . . . 7
⊢ (((𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 = (𝑁‘𝑥)) → 𝑦 ∈ 𝑋) |
24 | 23 | exp31 630 |
. . . . . 6
⊢ (𝐺 ∈ GrpOp → (𝑥 ∈ 𝑋 → (𝑦 = (𝑁‘𝑥) → 𝑦 ∈ 𝑋))) |
25 | 24 | rexlimdv 3030 |
. . . . 5
⊢ (𝐺 ∈ GrpOp →
(∃𝑥 ∈ 𝑋 𝑦 = (𝑁‘𝑥) → 𝑦 ∈ 𝑋)) |
26 | 19, 25 | impbid 202 |
. . . 4
⊢ (𝐺 ∈ GrpOp → (𝑦 ∈ 𝑋 ↔ ∃𝑥 ∈ 𝑋 𝑦 = (𝑁‘𝑥))) |
27 | 26 | abbi2dv 2742 |
. . 3
⊢ (𝐺 ∈ GrpOp → 𝑋 = {𝑦 ∣ ∃𝑥 ∈ 𝑋 𝑦 = (𝑁‘𝑥)}) |
28 | 11, 27 | eqtr4d 2659 |
. 2
⊢ (𝐺 ∈ GrpOp → ran 𝑁 = 𝑋) |
29 | | fveq2 6191 |
. . . 4
⊢ ((𝑁‘𝑥) = (𝑁‘𝑦) → (𝑁‘(𝑁‘𝑥)) = (𝑁‘(𝑁‘𝑦))) |
30 | 4, 6 | grpo2inv 27385 |
. . . . . 6
⊢ ((𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑁‘𝑥)) = 𝑥) |
31 | 30, 13 | eqeqan12d 2638 |
. . . . 5
⊢ (((𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋) ∧ (𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋)) → ((𝑁‘(𝑁‘𝑥)) = (𝑁‘(𝑁‘𝑦)) ↔ 𝑥 = 𝑦)) |
32 | 31 | anandis 873 |
. . . 4
⊢ ((𝐺 ∈ GrpOp ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑁‘(𝑁‘𝑥)) = (𝑁‘(𝑁‘𝑦)) ↔ 𝑥 = 𝑦)) |
33 | 29, 32 | syl5ib 234 |
. . 3
⊢ ((𝐺 ∈ GrpOp ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑁‘𝑥) = (𝑁‘𝑦) → 𝑥 = 𝑦)) |
34 | 33 | ralrimivva 2971 |
. 2
⊢ (𝐺 ∈ GrpOp →
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑁‘𝑥) = (𝑁‘𝑦) → 𝑥 = 𝑦)) |
35 | | dff1o6 6531 |
. 2
⊢ (𝑁:𝑋–1-1-onto→𝑋 ↔ (𝑁 Fn 𝑋 ∧ ran 𝑁 = 𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑁‘𝑥) = (𝑁‘𝑦) → 𝑥 = 𝑦))) |
36 | 9, 28, 34, 35 | syl3anbrc 1246 |
1
⊢ (𝐺 ∈ GrpOp → 𝑁:𝑋–1-1-onto→𝑋) |