Step | Hyp | Ref
| Expression |
1 | | inss1 4143 |
. . . 4
⊢ (Magma
∩ ExId ) ⊆ Magma |
2 | 1 | sseli 3896 |
. . 3
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ 𝐺 ∈
Magma) |
3 | | opidonOLD.1 |
. . . . 5
⊢ 𝑋 = dom dom 𝐺 |
4 | 3 | ismgmOLD 35745 |
. . . 4
⊢ (𝐺 ∈ Magma → (𝐺 ∈ Magma ↔ 𝐺:(𝑋 × 𝑋)⟶𝑋)) |
5 | 4 | ibi 270 |
. . 3
⊢ (𝐺 ∈ Magma → 𝐺:(𝑋 × 𝑋)⟶𝑋) |
6 | 2, 5 | syl 17 |
. 2
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ 𝐺:(𝑋 × 𝑋)⟶𝑋) |
7 | | inss2 4144 |
. . . . 5
⊢ (Magma
∩ ExId ) ⊆ ExId |
8 | 7 | sseli 3896 |
. . . 4
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ 𝐺 ∈ ExId
) |
9 | 3 | isexid 35742 |
. . . . 5
⊢ (𝐺 ∈ ExId → (𝐺 ∈ ExId ↔ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥))) |
10 | 9 | biimpd 232 |
. . . 4
⊢ (𝐺 ∈ ExId → (𝐺 ∈ ExId → ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥))) |
11 | 8, 8, 10 | sylc 65 |
. . 3
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ ∃𝑢 ∈
𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)) |
12 | | simpl 486 |
. . . . . . . 8
⊢ (((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) → (𝑢𝐺𝑥) = 𝑥) |
13 | 12 | ralimi 3083 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) → ∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥) |
14 | | oveq2 7221 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑢𝐺𝑥) = (𝑢𝐺𝑦)) |
15 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
16 | 14, 15 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑢𝐺𝑥) = 𝑥 ↔ (𝑢𝐺𝑦) = 𝑦)) |
17 | 16 | rspcv 3532 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥 → (𝑢𝐺𝑦) = 𝑦)) |
18 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑢𝐺𝑥) ↔ (𝑢𝐺𝑥) = 𝑦) |
19 | 14 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝑢𝐺𝑥) = 𝑦 ↔ (𝑢𝐺𝑦) = 𝑦)) |
20 | 18, 19 | syl5bb 286 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑦 = (𝑢𝐺𝑥) ↔ (𝑢𝐺𝑦) = 𝑦)) |
21 | 20 | rspcev 3537 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝑋 ∧ (𝑢𝐺𝑦) = 𝑦) → ∃𝑥 ∈ 𝑋 𝑦 = (𝑢𝐺𝑥)) |
22 | 21 | ex 416 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑋 → ((𝑢𝐺𝑦) = 𝑦 → ∃𝑥 ∈ 𝑋 𝑦 = (𝑢𝐺𝑥))) |
23 | 17, 22 | syld 47 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥 → ∃𝑥 ∈ 𝑋 𝑦 = (𝑢𝐺𝑥))) |
24 | 13, 23 | syl5 34 |
. . . . . 6
⊢ (𝑦 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) → ∃𝑥 ∈ 𝑋 𝑦 = (𝑢𝐺𝑥))) |
25 | 24 | reximdv 3192 |
. . . . 5
⊢ (𝑦 ∈ 𝑋 → (∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) → ∃𝑢 ∈ 𝑋 ∃𝑥 ∈ 𝑋 𝑦 = (𝑢𝐺𝑥))) |
26 | 25 | impcom 411 |
. . . 4
⊢
((∃𝑢 ∈
𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) ∧ 𝑦 ∈ 𝑋) → ∃𝑢 ∈ 𝑋 ∃𝑥 ∈ 𝑋 𝑦 = (𝑢𝐺𝑥)) |
27 | 26 | ralrimiva 3105 |
. . 3
⊢
(∃𝑢 ∈
𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) → ∀𝑦 ∈ 𝑋 ∃𝑢 ∈ 𝑋 ∃𝑥 ∈ 𝑋 𝑦 = (𝑢𝐺𝑥)) |
28 | 11, 27 | syl 17 |
. 2
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ ∀𝑦 ∈
𝑋 ∃𝑢 ∈ 𝑋 ∃𝑥 ∈ 𝑋 𝑦 = (𝑢𝐺𝑥)) |
29 | | foov 7382 |
. 2
⊢ (𝐺:(𝑋 × 𝑋)–onto→𝑋 ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑦 ∈ 𝑋 ∃𝑢 ∈ 𝑋 ∃𝑥 ∈ 𝑋 𝑦 = (𝑢𝐺𝑥))) |
30 | 6, 28, 29 | sylanbrc 586 |
1
⊢ (𝐺 ∈ (Magma ∩ ExId )
→ 𝐺:(𝑋 × 𝑋)–onto→𝑋) |