| Step | Hyp | Ref
| Expression |
| 1 | | riotaex 7392 |
. . . 4
⊢
(℩𝑦
∈ 𝑋 (𝑦𝐺𝑥) = (GId‘𝐺)) ∈ V |
| 2 | | eqid 2737 |
. . . 4
⊢ (𝑥 ∈ 𝑋 ↦ (℩𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = (GId‘𝐺))) = (𝑥 ∈ 𝑋 ↦ (℩𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = (GId‘𝐺))) |
| 3 | 1, 2 | fnmpti 6711 |
. . 3
⊢ (𝑥 ∈ 𝑋 ↦ (℩𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = (GId‘𝐺))) Fn 𝑋 |
| 4 | | grpasscan1.1 |
. . . . 5
⊢ 𝑋 = ran 𝐺 |
| 5 | | eqid 2737 |
. . . . 5
⊢
(GId‘𝐺) =
(GId‘𝐺) |
| 6 | | grpasscan1.2 |
. . . . 5
⊢ 𝑁 = (inv‘𝐺) |
| 7 | 4, 5, 6 | grpoinvfval 30541 |
. . . 4
⊢ (𝐺 ∈ GrpOp → 𝑁 = (𝑥 ∈ 𝑋 ↦ (℩𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = (GId‘𝐺)))) |
| 8 | 7 | fneq1d 6661 |
. . 3
⊢ (𝐺 ∈ GrpOp → (𝑁 Fn 𝑋 ↔ (𝑥 ∈ 𝑋 ↦ (℩𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = (GId‘𝐺))) Fn 𝑋)) |
| 9 | 3, 8 | mpbiri 258 |
. 2
⊢ (𝐺 ∈ GrpOp → 𝑁 Fn 𝑋) |
| 10 | | fnrnfv 6968 |
. . . 4
⊢ (𝑁 Fn 𝑋 → ran 𝑁 = {𝑦 ∣ ∃𝑥 ∈ 𝑋 𝑦 = (𝑁‘𝑥)}) |
| 11 | 9, 10 | syl 17 |
. . 3
⊢ (𝐺 ∈ GrpOp → ran 𝑁 = {𝑦 ∣ ∃𝑥 ∈ 𝑋 𝑦 = (𝑁‘𝑥)}) |
| 12 | 4, 6 | grpoinvcl 30543 |
. . . . . . 7
⊢ ((𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ 𝑋) |
| 13 | 4, 6 | grpo2inv 30550 |
. . . . . . . 8
⊢ ((𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋) → (𝑁‘(𝑁‘𝑦)) = 𝑦) |
| 14 | 13 | eqcomd 2743 |
. . . . . . 7
⊢ ((𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋) → 𝑦 = (𝑁‘(𝑁‘𝑦))) |
| 15 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑥 = (𝑁‘𝑦) → (𝑁‘𝑥) = (𝑁‘(𝑁‘𝑦))) |
| 16 | 15 | rspceeqv 3645 |
. . . . . . 7
⊢ (((𝑁‘𝑦) ∈ 𝑋 ∧ 𝑦 = (𝑁‘(𝑁‘𝑦))) → ∃𝑥 ∈ 𝑋 𝑦 = (𝑁‘𝑥)) |
| 17 | 12, 14, 16 | syl2anc 584 |
. . . . . 6
⊢ ((𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋) → ∃𝑥 ∈ 𝑋 𝑦 = (𝑁‘𝑥)) |
| 18 | 17 | ex 412 |
. . . . 5
⊢ (𝐺 ∈ GrpOp → (𝑦 ∈ 𝑋 → ∃𝑥 ∈ 𝑋 𝑦 = (𝑁‘𝑥))) |
| 19 | | simpr 484 |
. . . . . . 7
⊢ (((𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 = (𝑁‘𝑥)) → 𝑦 = (𝑁‘𝑥)) |
| 20 | 4, 6 | grpoinvcl 30543 |
. . . . . . . 8
⊢ ((𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋) → (𝑁‘𝑥) ∈ 𝑋) |
| 21 | 20 | adantr 480 |
. . . . . . 7
⊢ (((𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 = (𝑁‘𝑥)) → (𝑁‘𝑥) ∈ 𝑋) |
| 22 | 19, 21 | eqeltrd 2841 |
. . . . . 6
⊢ (((𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 = (𝑁‘𝑥)) → 𝑦 ∈ 𝑋) |
| 23 | 22 | rexlimdva2 3157 |
. . . . 5
⊢ (𝐺 ∈ GrpOp →
(∃𝑥 ∈ 𝑋 𝑦 = (𝑁‘𝑥) → 𝑦 ∈ 𝑋)) |
| 24 | 18, 23 | impbid 212 |
. . . 4
⊢ (𝐺 ∈ GrpOp → (𝑦 ∈ 𝑋 ↔ ∃𝑥 ∈ 𝑋 𝑦 = (𝑁‘𝑥))) |
| 25 | 24 | eqabdv 2875 |
. . 3
⊢ (𝐺 ∈ GrpOp → 𝑋 = {𝑦 ∣ ∃𝑥 ∈ 𝑋 𝑦 = (𝑁‘𝑥)}) |
| 26 | 11, 25 | eqtr4d 2780 |
. 2
⊢ (𝐺 ∈ GrpOp → ran 𝑁 = 𝑋) |
| 27 | | fveq2 6906 |
. . . 4
⊢ ((𝑁‘𝑥) = (𝑁‘𝑦) → (𝑁‘(𝑁‘𝑥)) = (𝑁‘(𝑁‘𝑦))) |
| 28 | 4, 6 | grpo2inv 30550 |
. . . . . 6
⊢ ((𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑁‘𝑥)) = 𝑥) |
| 29 | 28, 13 | eqeqan12d 2751 |
. . . . 5
⊢ (((𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋) ∧ (𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋)) → ((𝑁‘(𝑁‘𝑥)) = (𝑁‘(𝑁‘𝑦)) ↔ 𝑥 = 𝑦)) |
| 30 | 29 | anandis 678 |
. . . 4
⊢ ((𝐺 ∈ GrpOp ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑁‘(𝑁‘𝑥)) = (𝑁‘(𝑁‘𝑦)) ↔ 𝑥 = 𝑦)) |
| 31 | 27, 30 | imbitrid 244 |
. . 3
⊢ ((𝐺 ∈ GrpOp ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑁‘𝑥) = (𝑁‘𝑦) → 𝑥 = 𝑦)) |
| 32 | 31 | ralrimivva 3202 |
. 2
⊢ (𝐺 ∈ GrpOp →
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑁‘𝑥) = (𝑁‘𝑦) → 𝑥 = 𝑦)) |
| 33 | | dff1o6 7295 |
. 2
⊢ (𝑁:𝑋–1-1-onto→𝑋 ↔ (𝑁 Fn 𝑋 ∧ ran 𝑁 = 𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑁‘𝑥) = (𝑁‘𝑦) → 𝑥 = 𝑦))) |
| 34 | 9, 26, 32, 33 | syl3anbrc 1344 |
1
⊢ (𝐺 ∈ GrpOp → 𝑁:𝑋–1-1-onto→𝑋) |