Step | Hyp | Ref
| Expression |
1 | | feq1 6026 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (𝑔:(𝑡 × 𝑡)⟶𝑡 ↔ 𝐺:(𝑡 × 𝑡)⟶𝑡)) |
2 | | oveq 6656 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → ((𝑥𝑔𝑦)𝑔𝑧) = ((𝑥𝑔𝑦)𝐺𝑧)) |
3 | | oveq 6656 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (𝑥𝑔𝑦) = (𝑥𝐺𝑦)) |
4 | 3 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → ((𝑥𝑔𝑦)𝐺𝑧) = ((𝑥𝐺𝑦)𝐺𝑧)) |
5 | 2, 4 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → ((𝑥𝑔𝑦)𝑔𝑧) = ((𝑥𝐺𝑦)𝐺𝑧)) |
6 | | oveq 6656 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑥𝑔(𝑦𝑔𝑧)) = (𝑥𝐺(𝑦𝑔𝑧))) |
7 | | oveq 6656 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (𝑦𝑔𝑧) = (𝑦𝐺𝑧)) |
8 | 7 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑥𝐺(𝑦𝑔𝑧)) = (𝑥𝐺(𝑦𝐺𝑧))) |
9 | 6, 8 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑥𝑔(𝑦𝑔𝑧)) = (𝑥𝐺(𝑦𝐺𝑧))) |
10 | 5, 9 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ↔ ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))) |
11 | 10 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ↔ ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))) |
12 | 11 | 2ralbidv 2989 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ↔ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))) |
13 | | oveq 6656 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑢𝑔𝑥) = (𝑢𝐺𝑥)) |
14 | 13 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ((𝑢𝑔𝑥) = 𝑥 ↔ (𝑢𝐺𝑥) = 𝑥)) |
15 | | oveq 6656 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑦𝑔𝑥) = (𝑦𝐺𝑥)) |
16 | 15 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → ((𝑦𝑔𝑥) = 𝑢 ↔ (𝑦𝐺𝑥) = 𝑢)) |
17 | 16 | rexbidv 3052 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢 ↔ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) |
18 | 14, 17 | anbi12d 747 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢) ↔ ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢))) |
19 | 18 | rexralbidv 3058 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢) ↔ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢))) |
20 | 1, 12, 19 | 3anbi123d 1399 |
. . . . 5
⊢ (𝑔 = 𝐺 → ((𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢)) ↔ (𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)))) |
21 | 20 | exbidv 1850 |
. . . 4
⊢ (𝑔 = 𝐺 → (∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢)) ↔ ∃𝑡(𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)))) |
22 | | df-grpo 27347 |
. . . 4
⊢ GrpOp =
{𝑔 ∣ ∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢))} |
23 | 21, 22 | elab2g 3353 |
. . 3
⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ GrpOp ↔ ∃𝑡(𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)))) |
24 | | simpl 473 |
. . . . . . . . . . . . . 14
⊢ (((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) → (𝑢𝐺𝑥) = 𝑥) |
25 | 24 | ralimi 2952 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) → ∀𝑥 ∈ 𝑡 (𝑢𝐺𝑥) = 𝑥) |
26 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → (𝑢𝐺𝑥) = (𝑢𝐺𝑧)) |
27 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧) |
28 | 26, 27 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → ((𝑢𝐺𝑥) = 𝑥 ↔ (𝑢𝐺𝑧) = 𝑧)) |
29 | | eqcom 2629 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢𝐺𝑧) = 𝑧 ↔ 𝑧 = (𝑢𝐺𝑧)) |
30 | 28, 29 | syl6bb 276 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → ((𝑢𝐺𝑥) = 𝑥 ↔ 𝑧 = (𝑢𝐺𝑧))) |
31 | 30 | rspcv 3305 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝑡 → (∀𝑥 ∈ 𝑡 (𝑢𝐺𝑥) = 𝑥 → 𝑧 = (𝑢𝐺𝑧))) |
32 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → (𝑢𝐺𝑦) = (𝑢𝐺𝑧)) |
33 | 32 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → (𝑧 = (𝑢𝐺𝑦) ↔ 𝑧 = (𝑢𝐺𝑧))) |
34 | 33 | rspcev 3309 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝑡 ∧ 𝑧 = (𝑢𝐺𝑧)) → ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦)) |
35 | 34 | ex 450 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝑡 → (𝑧 = (𝑢𝐺𝑧) → ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦))) |
36 | 31, 35 | syld 47 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑡 → (∀𝑥 ∈ 𝑡 (𝑢𝐺𝑥) = 𝑥 → ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦))) |
37 | 25, 36 | syl5 34 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑡 → (∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) → ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦))) |
38 | 37 | reximdv 3016 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑡 → (∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) → ∃𝑢 ∈ 𝑡 ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦))) |
39 | 38 | impcom 446 |
. . . . . . . . . 10
⊢
((∃𝑢 ∈
𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) ∧ 𝑧 ∈ 𝑡) → ∃𝑢 ∈ 𝑡 ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦)) |
40 | 39 | ralrimiva 2966 |
. . . . . . . . 9
⊢
(∃𝑢 ∈
𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) → ∀𝑧 ∈ 𝑡 ∃𝑢 ∈ 𝑡 ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦)) |
41 | 40 | anim2i 593 |
. . . . . . . 8
⊢ ((𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) → (𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑧 ∈ 𝑡 ∃𝑢 ∈ 𝑡 ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦))) |
42 | | foov 6808 |
. . . . . . . 8
⊢ (𝐺:(𝑡 × 𝑡)–onto→𝑡 ↔ (𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑧 ∈ 𝑡 ∃𝑢 ∈ 𝑡 ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦))) |
43 | 41, 42 | sylibr 224 |
. . . . . . 7
⊢ ((𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) → 𝐺:(𝑡 × 𝑡)–onto→𝑡) |
44 | | forn 6118 |
. . . . . . . 8
⊢ (𝐺:(𝑡 × 𝑡)–onto→𝑡 → ran 𝐺 = 𝑡) |
45 | 44 | eqcomd 2628 |
. . . . . . 7
⊢ (𝐺:(𝑡 × 𝑡)–onto→𝑡 → 𝑡 = ran 𝐺) |
46 | 43, 45 | syl 17 |
. . . . . 6
⊢ ((𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) → 𝑡 = ran 𝐺) |
47 | 46 | 3adant2 1080 |
. . . . 5
⊢ ((𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) → 𝑡 = ran 𝐺) |
48 | 47 | pm4.71ri 665 |
. . . 4
⊢ ((𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) ↔ (𝑡 = ran 𝐺 ∧ (𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)))) |
49 | 48 | exbii 1774 |
. . 3
⊢
(∃𝑡(𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) ↔ ∃𝑡(𝑡 = ran 𝐺 ∧ (𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)))) |
50 | 23, 49 | syl6bb 276 |
. 2
⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ GrpOp ↔ ∃𝑡(𝑡 = ran 𝐺 ∧ (𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢))))) |
51 | | rnexg 7098 |
. . 3
⊢ (𝐺 ∈ 𝐴 → ran 𝐺 ∈ V) |
52 | | isgrp.1 |
. . . . . 6
⊢ 𝑋 = ran 𝐺 |
53 | 52 | eqeq2i 2634 |
. . . . 5
⊢ (𝑡 = 𝑋 ↔ 𝑡 = ran 𝐺) |
54 | | xpeq1 5128 |
. . . . . . . . 9
⊢ (𝑡 = 𝑋 → (𝑡 × 𝑡) = (𝑋 × 𝑡)) |
55 | | xpeq2 5129 |
. . . . . . . . 9
⊢ (𝑡 = 𝑋 → (𝑋 × 𝑡) = (𝑋 × 𝑋)) |
56 | 54, 55 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝑡 = 𝑋 → (𝑡 × 𝑡) = (𝑋 × 𝑋)) |
57 | 56 | feq2d 6031 |
. . . . . . 7
⊢ (𝑡 = 𝑋 → (𝐺:(𝑡 × 𝑡)⟶𝑡 ↔ 𝐺:(𝑋 × 𝑋)⟶𝑡)) |
58 | | feq3 6028 |
. . . . . . 7
⊢ (𝑡 = 𝑋 → (𝐺:(𝑋 × 𝑋)⟶𝑡 ↔ 𝐺:(𝑋 × 𝑋)⟶𝑋)) |
59 | 57, 58 | bitrd 268 |
. . . . . 6
⊢ (𝑡 = 𝑋 → (𝐺:(𝑡 × 𝑡)⟶𝑡 ↔ 𝐺:(𝑋 × 𝑋)⟶𝑋)) |
60 | | raleq 3138 |
. . . . . . . 8
⊢ (𝑡 = 𝑋 → (∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ↔ ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))) |
61 | 60 | raleqbi1dv 3146 |
. . . . . . 7
⊢ (𝑡 = 𝑋 → (∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))) |
62 | 61 | raleqbi1dv 3146 |
. . . . . 6
⊢ (𝑡 = 𝑋 → (∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))) |
63 | | rexeq 3139 |
. . . . . . . . 9
⊢ (𝑡 = 𝑋 → (∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢 ↔ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)) |
64 | 63 | anbi2d 740 |
. . . . . . . 8
⊢ (𝑡 = 𝑋 → (((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) ↔ ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢))) |
65 | 64 | raleqbi1dv 3146 |
. . . . . . 7
⊢ (𝑡 = 𝑋 → (∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) ↔ ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢))) |
66 | 65 | rexeqbi1dv 3147 |
. . . . . 6
⊢ (𝑡 = 𝑋 → (∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) ↔ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢))) |
67 | 59, 62, 66 | 3anbi123d 1399 |
. . . . 5
⊢ (𝑡 = 𝑋 → ((𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)))) |
68 | 53, 67 | sylbir 225 |
. . . 4
⊢ (𝑡 = ran 𝐺 → ((𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)))) |
69 | 68 | ceqsexgv 3335 |
. . 3
⊢ (ran
𝐺 ∈ V →
(∃𝑡(𝑡 = ran 𝐺 ∧ (𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢))) ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)))) |
70 | 51, 69 | syl 17 |
. 2
⊢ (𝐺 ∈ 𝐴 → (∃𝑡(𝑡 = ran 𝐺 ∧ (𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢))) ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)))) |
71 | 50, 70 | bitrd 268 |
1
⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ GrpOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)))) |