Step | Hyp | Ref
| Expression |
1 | | isgrpoi.2 |
. 2
⊢ 𝐺:(𝑋 × 𝑋)⟶𝑋 |
2 | | isgrpoi.3 |
. . 3
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))) |
3 | 2 | rgen3 3125 |
. 2
⊢
∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) |
4 | | isgrpoi.4 |
. . 3
⊢ 𝑈 ∈ 𝑋 |
5 | | isgrpoi.5 |
. . . . 5
⊢ (𝑥 ∈ 𝑋 → (𝑈𝐺𝑥) = 𝑥) |
6 | | isgrpoi.6 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋 → 𝑁 ∈ 𝑋) |
7 | | isgrpoi.7 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋 → (𝑁𝐺𝑥) = 𝑈) |
8 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑦 = 𝑁 → (𝑦𝐺𝑥) = (𝑁𝐺𝑥)) |
9 | 8 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑦 = 𝑁 → ((𝑦𝐺𝑥) = 𝑈 ↔ (𝑁𝐺𝑥) = 𝑈)) |
10 | 9 | rspcev 3537 |
. . . . . 6
⊢ ((𝑁 ∈ 𝑋 ∧ (𝑁𝐺𝑥) = 𝑈) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈) |
11 | 6, 7, 10 | syl2anc 587 |
. . . . 5
⊢ (𝑥 ∈ 𝑋 → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈) |
12 | 5, 11 | jca 515 |
. . . 4
⊢ (𝑥 ∈ 𝑋 → ((𝑈𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)) |
13 | 12 | rgen 3071 |
. . 3
⊢
∀𝑥 ∈
𝑋 ((𝑈𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈) |
14 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑢 = 𝑈 → (𝑢𝐺𝑥) = (𝑈𝐺𝑥)) |
15 | 14 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑢 = 𝑈 → ((𝑢𝐺𝑥) = 𝑥 ↔ (𝑈𝐺𝑥) = 𝑥)) |
16 | | eqeq2 2749 |
. . . . . . 7
⊢ (𝑢 = 𝑈 → ((𝑦𝐺𝑥) = 𝑢 ↔ (𝑦𝐺𝑥) = 𝑈)) |
17 | 16 | rexbidv 3216 |
. . . . . 6
⊢ (𝑢 = 𝑈 → (∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢 ↔ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)) |
18 | 15, 17 | anbi12d 634 |
. . . . 5
⊢ (𝑢 = 𝑈 → (((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢) ↔ ((𝑈𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈))) |
19 | 18 | ralbidv 3118 |
. . . 4
⊢ (𝑢 = 𝑈 → (∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢) ↔ ∀𝑥 ∈ 𝑋 ((𝑈𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈))) |
20 | 19 | rspcev 3537 |
. . 3
⊢ ((𝑈 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝑋 ((𝑈𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)) → ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)) |
21 | 4, 13, 20 | mp2an 692 |
. 2
⊢
∃𝑢 ∈
𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢) |
22 | | isgrpoi.1 |
. . . . 5
⊢ 𝑋 ∈ V |
23 | 22, 22 | xpex 7538 |
. . . 4
⊢ (𝑋 × 𝑋) ∈ V |
24 | | fex 7042 |
. . . 4
⊢ ((𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ (𝑋 × 𝑋) ∈ V) → 𝐺 ∈ V) |
25 | 1, 23, 24 | mp2an 692 |
. . 3
⊢ 𝐺 ∈ V |
26 | 5 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋 → 𝑥 = (𝑈𝐺𝑥)) |
27 | | rspceov 7260 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑥 = (𝑈𝐺𝑥)) → ∃𝑦 ∈ 𝑋 ∃𝑧 ∈ 𝑋 𝑥 = (𝑦𝐺𝑧)) |
28 | 4, 27 | mp3an1 1450 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑥 = (𝑈𝐺𝑥)) → ∃𝑦 ∈ 𝑋 ∃𝑧 ∈ 𝑋 𝑥 = (𝑦𝐺𝑧)) |
29 | 26, 28 | mpdan 687 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑋 → ∃𝑦 ∈ 𝑋 ∃𝑧 ∈ 𝑋 𝑥 = (𝑦𝐺𝑧)) |
30 | 29 | rgen 3071 |
. . . . . . 7
⊢
∀𝑥 ∈
𝑋 ∃𝑦 ∈ 𝑋 ∃𝑧 ∈ 𝑋 𝑥 = (𝑦𝐺𝑧) |
31 | | foov 7382 |
. . . . . . 7
⊢ (𝐺:(𝑋 × 𝑋)–onto→𝑋 ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ∃𝑧 ∈ 𝑋 𝑥 = (𝑦𝐺𝑧))) |
32 | 1, 30, 31 | mpbir2an 711 |
. . . . . 6
⊢ 𝐺:(𝑋 × 𝑋)–onto→𝑋 |
33 | | forn 6636 |
. . . . . 6
⊢ (𝐺:(𝑋 × 𝑋)–onto→𝑋 → ran 𝐺 = 𝑋) |
34 | 32, 33 | ax-mp 5 |
. . . . 5
⊢ ran 𝐺 = 𝑋 |
35 | 34 | eqcomi 2746 |
. . . 4
⊢ 𝑋 = ran 𝐺 |
36 | 35 | isgrpo 28578 |
. . 3
⊢ (𝐺 ∈ V → (𝐺 ∈ GrpOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)))) |
37 | 25, 36 | ax-mp 5 |
. 2
⊢ (𝐺 ∈ GrpOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢))) |
38 | 1, 3, 21, 37 | mpbir3an 1343 |
1
⊢ 𝐺 ∈ GrpOp |