Step | Hyp | Ref
| Expression |
1 | | exidu1.1 |
. . 3
⊢ 𝑋 = ran 𝐺 |
2 | 1 | isexid2 36013 |
. 2
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ ∃𝑢 ∈
𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)) |
3 | | simpl 483 |
. . . . . . 7
⊢ (((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) → (𝑢𝐺𝑥) = 𝑥) |
4 | 3 | ralimi 3087 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) → ∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥) |
5 | | oveq2 7283 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑢𝐺𝑥) = (𝑢𝐺𝑦)) |
6 | | id 22 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
7 | 5, 6 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑢𝐺𝑥) = 𝑥 ↔ (𝑢𝐺𝑦) = 𝑦)) |
8 | 7 | rspcv 3557 |
. . . . . 6
⊢ (𝑦 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥 → (𝑢𝐺𝑦) = 𝑦)) |
9 | 4, 8 | syl5 34 |
. . . . 5
⊢ (𝑦 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) → (𝑢𝐺𝑦) = 𝑦)) |
10 | | simpr 485 |
. . . . . . 7
⊢ (((𝑦𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑦) = 𝑥) → (𝑥𝐺𝑦) = 𝑥) |
11 | 10 | ralimi 3087 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 ((𝑦𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑦) = 𝑥) → ∀𝑥 ∈ 𝑋 (𝑥𝐺𝑦) = 𝑥) |
12 | | oveq1 7282 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → (𝑥𝐺𝑦) = (𝑢𝐺𝑦)) |
13 | | id 22 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → 𝑥 = 𝑢) |
14 | 12, 13 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑥 = 𝑢 → ((𝑥𝐺𝑦) = 𝑥 ↔ (𝑢𝐺𝑦) = 𝑢)) |
15 | 14 | rspcv 3557 |
. . . . . 6
⊢ (𝑢 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑥𝐺𝑦) = 𝑥 → (𝑢𝐺𝑦) = 𝑢)) |
16 | 11, 15 | syl5 34 |
. . . . 5
⊢ (𝑢 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 ((𝑦𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑦) = 𝑥) → (𝑢𝐺𝑦) = 𝑢)) |
17 | 9, 16 | im2anan9r 621 |
. . . 4
⊢ ((𝑢 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑦) = 𝑥)) → ((𝑢𝐺𝑦) = 𝑦 ∧ (𝑢𝐺𝑦) = 𝑢))) |
18 | | eqtr2 2762 |
. . . . 5
⊢ (((𝑢𝐺𝑦) = 𝑦 ∧ (𝑢𝐺𝑦) = 𝑢) → 𝑦 = 𝑢) |
19 | 18 | equcomd 2022 |
. . . 4
⊢ (((𝑢𝐺𝑦) = 𝑦 ∧ (𝑢𝐺𝑦) = 𝑢) → 𝑢 = 𝑦) |
20 | 17, 19 | syl6 35 |
. . 3
⊢ ((𝑢 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑦) = 𝑥)) → 𝑢 = 𝑦)) |
21 | 20 | rgen2 3120 |
. 2
⊢
∀𝑢 ∈
𝑋 ∀𝑦 ∈ 𝑋 ((∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑦) = 𝑥)) → 𝑢 = 𝑦) |
22 | | oveq1 7282 |
. . . . 5
⊢ (𝑢 = 𝑦 → (𝑢𝐺𝑥) = (𝑦𝐺𝑥)) |
23 | 22 | eqeq1d 2740 |
. . . 4
⊢ (𝑢 = 𝑦 → ((𝑢𝐺𝑥) = 𝑥 ↔ (𝑦𝐺𝑥) = 𝑥)) |
24 | 23 | ovanraleqv 7299 |
. . 3
⊢ (𝑢 = 𝑦 → (∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) ↔ ∀𝑥 ∈ 𝑋 ((𝑦𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑦) = 𝑥))) |
25 | 24 | reu4 3666 |
. 2
⊢
(∃!𝑢 ∈
𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) ↔ (∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) ∧ ∀𝑢 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑦) = 𝑥)) → 𝑢 = 𝑦))) |
26 | 2, 21, 25 | sylanblrc 590 |
1
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ ∃!𝑢 ∈
𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)) |