Step | Hyp | Ref
| Expression |
1 | | feq1 6485 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (𝑔:(𝑡 × 𝑡)⟶𝑡 ↔ 𝐺:(𝑡 × 𝑡)⟶𝑡)) |
2 | | oveq 7176 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → ((𝑥𝑔𝑦)𝑔𝑧) = ((𝑥𝑔𝑦)𝐺𝑧)) |
3 | | oveq 7176 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (𝑥𝑔𝑦) = (𝑥𝐺𝑦)) |
4 | 3 | oveq1d 7185 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → ((𝑥𝑔𝑦)𝐺𝑧) = ((𝑥𝐺𝑦)𝐺𝑧)) |
5 | 2, 4 | eqtrd 2773 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → ((𝑥𝑔𝑦)𝑔𝑧) = ((𝑥𝐺𝑦)𝐺𝑧)) |
6 | | oveq 7176 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑥𝑔(𝑦𝑔𝑧)) = (𝑥𝐺(𝑦𝑔𝑧))) |
7 | | oveq 7176 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (𝑦𝑔𝑧) = (𝑦𝐺𝑧)) |
8 | 7 | oveq2d 7186 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑥𝐺(𝑦𝑔𝑧)) = (𝑥𝐺(𝑦𝐺𝑧))) |
9 | 6, 8 | eqtrd 2773 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑥𝑔(𝑦𝑔𝑧)) = (𝑥𝐺(𝑦𝐺𝑧))) |
10 | 5, 9 | eqeq12d 2754 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ↔ ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))) |
11 | 10 | ralbidv 3109 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ↔ ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))) |
12 | 11 | 2ralbidv 3111 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ↔ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))) |
13 | | oveq 7176 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑢𝑔𝑥) = (𝑢𝐺𝑥)) |
14 | 13 | eqeq1d 2740 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ((𝑢𝑔𝑥) = 𝑥 ↔ (𝑢𝐺𝑥) = 𝑥)) |
15 | | oveq 7176 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑦𝑔𝑥) = (𝑦𝐺𝑥)) |
16 | 15 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → ((𝑦𝑔𝑥) = 𝑢 ↔ (𝑦𝐺𝑥) = 𝑢)) |
17 | 16 | rexbidv 3207 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢 ↔ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) |
18 | 14, 17 | anbi12d 634 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢) ↔ ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢))) |
19 | 18 | rexralbidv 3211 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢) ↔ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢))) |
20 | 1, 12, 19 | 3anbi123d 1437 |
. . . . 5
⊢ (𝑔 = 𝐺 → ((𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢)) ↔ (𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)))) |
21 | 20 | exbidv 1928 |
. . . 4
⊢ (𝑔 = 𝐺 → (∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢)) ↔ ∃𝑡(𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)))) |
22 | | df-grpo 28428 |
. . . 4
⊢ GrpOp =
{𝑔 ∣ ∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢))} |
23 | 21, 22 | elab2g 3575 |
. . 3
⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ GrpOp ↔ ∃𝑡(𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)))) |
24 | | simpl 486 |
. . . . . . . . . . . . . 14
⊢ (((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) → (𝑢𝐺𝑥) = 𝑥) |
25 | 24 | ralimi 3075 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) → ∀𝑥 ∈ 𝑡 (𝑢𝐺𝑥) = 𝑥) |
26 | | oveq2 7178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → (𝑢𝐺𝑥) = (𝑢𝐺𝑧)) |
27 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧) |
28 | 26, 27 | eqeq12d 2754 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → ((𝑢𝐺𝑥) = 𝑥 ↔ (𝑢𝐺𝑧) = 𝑧)) |
29 | | eqcom 2745 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢𝐺𝑧) = 𝑧 ↔ 𝑧 = (𝑢𝐺𝑧)) |
30 | 28, 29 | bitrdi 290 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → ((𝑢𝐺𝑥) = 𝑥 ↔ 𝑧 = (𝑢𝐺𝑧))) |
31 | 30 | rspcv 3521 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝑡 → (∀𝑥 ∈ 𝑡 (𝑢𝐺𝑥) = 𝑥 → 𝑧 = (𝑢𝐺𝑧))) |
32 | | oveq2 7178 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → (𝑢𝐺𝑦) = (𝑢𝐺𝑧)) |
33 | 32 | rspceeqv 3541 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝑡 ∧ 𝑧 = (𝑢𝐺𝑧)) → ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦)) |
34 | 33 | ex 416 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝑡 → (𝑧 = (𝑢𝐺𝑧) → ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦))) |
35 | 31, 34 | syld 47 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑡 → (∀𝑥 ∈ 𝑡 (𝑢𝐺𝑥) = 𝑥 → ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦))) |
36 | 25, 35 | syl5 34 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑡 → (∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) → ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦))) |
37 | 36 | reximdv 3183 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑡 → (∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) → ∃𝑢 ∈ 𝑡 ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦))) |
38 | 37 | impcom 411 |
. . . . . . . . . 10
⊢
((∃𝑢 ∈
𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) ∧ 𝑧 ∈ 𝑡) → ∃𝑢 ∈ 𝑡 ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦)) |
39 | 38 | ralrimiva 3096 |
. . . . . . . . 9
⊢
(∃𝑢 ∈
𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) → ∀𝑧 ∈ 𝑡 ∃𝑢 ∈ 𝑡 ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦)) |
40 | 39 | anim2i 620 |
. . . . . . . 8
⊢ ((𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) → (𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑧 ∈ 𝑡 ∃𝑢 ∈ 𝑡 ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦))) |
41 | | foov 7338 |
. . . . . . . 8
⊢ (𝐺:(𝑡 × 𝑡)–onto→𝑡 ↔ (𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑧 ∈ 𝑡 ∃𝑢 ∈ 𝑡 ∃𝑦 ∈ 𝑡 𝑧 = (𝑢𝐺𝑦))) |
42 | 40, 41 | sylibr 237 |
. . . . . . 7
⊢ ((𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) → 𝐺:(𝑡 × 𝑡)–onto→𝑡) |
43 | | forn 6595 |
. . . . . . . 8
⊢ (𝐺:(𝑡 × 𝑡)–onto→𝑡 → ran 𝐺 = 𝑡) |
44 | 43 | eqcomd 2744 |
. . . . . . 7
⊢ (𝐺:(𝑡 × 𝑡)–onto→𝑡 → 𝑡 = ran 𝐺) |
45 | 42, 44 | syl 17 |
. . . . . 6
⊢ ((𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) → 𝑡 = ran 𝐺) |
46 | 45 | 3adant2 1132 |
. . . . 5
⊢ ((𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) → 𝑡 = ran 𝐺) |
47 | 46 | pm4.71ri 564 |
. . . 4
⊢ ((𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) ↔ (𝑡 = ran 𝐺 ∧ (𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)))) |
48 | 47 | exbii 1854 |
. . 3
⊢
(∃𝑡(𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) ↔ ∃𝑡(𝑡 = ran 𝐺 ∧ (𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)))) |
49 | 23, 48 | bitrdi 290 |
. 2
⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ GrpOp ↔ ∃𝑡(𝑡 = ran 𝐺 ∧ (𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢))))) |
50 | | rnexg 7635 |
. . 3
⊢ (𝐺 ∈ 𝐴 → ran 𝐺 ∈ V) |
51 | | isgrp.1 |
. . . . . 6
⊢ 𝑋 = ran 𝐺 |
52 | 51 | eqeq2i 2751 |
. . . . 5
⊢ (𝑡 = 𝑋 ↔ 𝑡 = ran 𝐺) |
53 | | xpeq1 5539 |
. . . . . . . . 9
⊢ (𝑡 = 𝑋 → (𝑡 × 𝑡) = (𝑋 × 𝑡)) |
54 | | xpeq2 5546 |
. . . . . . . . 9
⊢ (𝑡 = 𝑋 → (𝑋 × 𝑡) = (𝑋 × 𝑋)) |
55 | 53, 54 | eqtrd 2773 |
. . . . . . . 8
⊢ (𝑡 = 𝑋 → (𝑡 × 𝑡) = (𝑋 × 𝑋)) |
56 | 55 | feq2d 6490 |
. . . . . . 7
⊢ (𝑡 = 𝑋 → (𝐺:(𝑡 × 𝑡)⟶𝑡 ↔ 𝐺:(𝑋 × 𝑋)⟶𝑡)) |
57 | | feq3 6487 |
. . . . . . 7
⊢ (𝑡 = 𝑋 → (𝐺:(𝑋 × 𝑋)⟶𝑡 ↔ 𝐺:(𝑋 × 𝑋)⟶𝑋)) |
58 | 56, 57 | bitrd 282 |
. . . . . 6
⊢ (𝑡 = 𝑋 → (𝐺:(𝑡 × 𝑡)⟶𝑡 ↔ 𝐺:(𝑋 × 𝑋)⟶𝑋)) |
59 | | raleq 3310 |
. . . . . . . 8
⊢ (𝑡 = 𝑋 → (∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ↔ ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))) |
60 | 59 | raleqbi1dv 3308 |
. . . . . . 7
⊢ (𝑡 = 𝑋 → (∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))) |
61 | 60 | raleqbi1dv 3308 |
. . . . . 6
⊢ (𝑡 = 𝑋 → (∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))) |
62 | | rexeq 3311 |
. . . . . . . . 9
⊢ (𝑡 = 𝑋 → (∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢 ↔ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)) |
63 | 62 | anbi2d 632 |
. . . . . . . 8
⊢ (𝑡 = 𝑋 → (((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) ↔ ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢))) |
64 | 63 | raleqbi1dv 3308 |
. . . . . . 7
⊢ (𝑡 = 𝑋 → (∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) ↔ ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢))) |
65 | 64 | rexeqbi1dv 3309 |
. . . . . 6
⊢ (𝑡 = 𝑋 → (∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢) ↔ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢))) |
66 | 58, 61, 65 | 3anbi123d 1437 |
. . . . 5
⊢ (𝑡 = 𝑋 → ((𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)))) |
67 | 52, 66 | sylbir 238 |
. . . 4
⊢ (𝑡 = ran 𝐺 → ((𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢)) ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)))) |
68 | 67 | ceqsexgv 3550 |
. . 3
⊢ (ran
𝐺 ∈ V →
(∃𝑡(𝑡 = ran 𝐺 ∧ (𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢))) ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)))) |
69 | 50, 68 | syl 17 |
. 2
⊢ (𝐺 ∈ 𝐴 → (∃𝑡(𝑡 = ran 𝐺 ∧ (𝐺:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝐺𝑥) = 𝑢))) ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)))) |
70 | 49, 69 | bitrd 282 |
1
⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ GrpOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)))) |