Step | Hyp | Ref
| Expression |
1 | | snex 5392 |
. 2
⊢ {𝐴} ∈ V |
2 | | opex 5425 |
. . . . 5
⊢
⟨𝐴, 𝐴⟩ ∈ V |
3 | | grposnOLD.1 |
. . . . 5
⊢ 𝐴 ∈ V |
4 | 2, 3 | f1osn 6828 |
. . . 4
⊢
{⟨⟨𝐴,
𝐴⟩, 𝐴⟩}:{⟨𝐴, 𝐴⟩}–1-1-onto→{𝐴} |
5 | | f1of 6788 |
. . . 4
⊢
({⟨⟨𝐴,
𝐴⟩, 𝐴⟩}:{⟨𝐴, 𝐴⟩}–1-1-onto→{𝐴} → {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}:{⟨𝐴, 𝐴⟩}⟶{𝐴}) |
6 | 4, 5 | ax-mp 5 |
. . 3
⊢
{⟨⟨𝐴,
𝐴⟩, 𝐴⟩}:{⟨𝐴, 𝐴⟩}⟶{𝐴} |
7 | 3, 3 | xpsn 7091 |
. . . 4
⊢ ({𝐴} × {𝐴}) = {⟨𝐴, 𝐴⟩} |
8 | 7 | feq2i 6664 |
. . 3
⊢
({⟨⟨𝐴,
𝐴⟩, 𝐴⟩}:({𝐴} × {𝐴})⟶{𝐴} ↔ {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}:{⟨𝐴, 𝐴⟩}⟶{𝐴}) |
9 | 6, 8 | mpbir 230 |
. 2
⊢
{⟨⟨𝐴,
𝐴⟩, 𝐴⟩}:({𝐴} × {𝐴})⟶{𝐴} |
10 | | velsn 4606 |
. . 3
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
11 | | velsn 4606 |
. . 3
⊢ (𝑦 ∈ {𝐴} ↔ 𝑦 = 𝐴) |
12 | | velsn 4606 |
. . 3
⊢ (𝑧 ∈ {𝐴} ↔ 𝑧 = 𝐴) |
13 | | oveq2 7369 |
. . . . . 6
⊢ (𝑧 = 𝐴 → ((𝑥{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑦){⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧) = ((𝑥{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑦){⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝐴)) |
14 | | oveq1 7368 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝑥{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑦) = (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑦)) |
15 | | oveq2 7369 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑦) = (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝐴)) |
16 | | df-ov 7364 |
. . . . . . . . . . 11
⊢ (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝐴) = ({⟨⟨𝐴, 𝐴⟩, 𝐴⟩}‘⟨𝐴, 𝐴⟩) |
17 | 2, 3 | fvsn 7131 |
. . . . . . . . . . 11
⊢
({⟨⟨𝐴,
𝐴⟩, 𝐴⟩}‘⟨𝐴, 𝐴⟩) = 𝐴 |
18 | 16, 17 | eqtri 2761 |
. . . . . . . . . 10
⊢ (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝐴) = 𝐴 |
19 | 15, 18 | eqtrdi 2789 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑦) = 𝐴) |
20 | 14, 19 | sylan9eq 2793 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → (𝑥{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑦) = 𝐴) |
21 | 20 | oveq1d 7376 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → ((𝑥{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑦){⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝐴) = (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝐴)) |
22 | 21, 18 | eqtrdi 2789 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → ((𝑥{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑦){⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝐴) = 𝐴) |
23 | 13, 22 | sylan9eqr 2795 |
. . . . 5
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) ∧ 𝑧 = 𝐴) → ((𝑥{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑦){⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧) = 𝐴) |
24 | 23 | 3impa 1111 |
. . . 4
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → ((𝑥{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑦){⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧) = 𝐴) |
25 | | oveq1 7368 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥{⟨⟨𝐴, 𝐴⟩, 𝐴⟩} (𝑦{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧)) = (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩} (𝑦{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧))) |
26 | | oveq1 7368 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → (𝑦{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧) = (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧)) |
27 | | oveq2 7369 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐴 → (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧) = (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝐴)) |
28 | 27, 18 | eqtrdi 2789 |
. . . . . . . . 9
⊢ (𝑧 = 𝐴 → (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧) = 𝐴) |
29 | 26, 28 | sylan9eq 2793 |
. . . . . . . 8
⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → (𝑦{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧) = 𝐴) |
30 | 29 | oveq2d 7377 |
. . . . . . 7
⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩} (𝑦{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧)) = (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝐴)) |
31 | 30, 18 | eqtrdi 2789 |
. . . . . 6
⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩} (𝑦{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧)) = 𝐴) |
32 | 25, 31 | sylan9eq 2793 |
. . . . 5
⊢ ((𝑥 = 𝐴 ∧ (𝑦 = 𝐴 ∧ 𝑧 = 𝐴)) → (𝑥{⟨⟨𝐴, 𝐴⟩, 𝐴⟩} (𝑦{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧)) = 𝐴) |
33 | 32 | 3impb 1116 |
. . . 4
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → (𝑥{⟨⟨𝐴, 𝐴⟩, 𝐴⟩} (𝑦{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧)) = 𝐴) |
34 | 24, 33 | eqtr4d 2776 |
. . 3
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → ((𝑥{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑦){⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧) = (𝑥{⟨⟨𝐴, 𝐴⟩, 𝐴⟩} (𝑦{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧))) |
35 | 10, 11, 12, 34 | syl3anb 1162 |
. 2
⊢ ((𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴} ∧ 𝑧 ∈ {𝐴}) → ((𝑥{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑦){⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧) = (𝑥{⟨⟨𝐴, 𝐴⟩, 𝐴⟩} (𝑦{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑧))) |
36 | 3 | snid 4626 |
. 2
⊢ 𝐴 ∈ {𝐴} |
37 | | oveq2 7369 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑥) = (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝐴)) |
38 | 37, 18 | eqtrdi 2789 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑥) = 𝐴) |
39 | | id 22 |
. . . 4
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) |
40 | 38, 39 | eqtr4d 2776 |
. . 3
⊢ (𝑥 = 𝐴 → (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑥) = 𝑥) |
41 | 10, 40 | sylbi 216 |
. 2
⊢ (𝑥 ∈ {𝐴} → (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑥) = 𝑥) |
42 | 36 | a1i 11 |
. 2
⊢ (𝑥 ∈ {𝐴} → 𝐴 ∈ {𝐴}) |
43 | 10, 38 | sylbi 216 |
. 2
⊢ (𝑥 ∈ {𝐴} → (𝐴{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}𝑥) = 𝐴) |
44 | 1, 9, 35, 36, 41, 42, 43 | isgrpoi 29489 |
1
⊢
{⟨⟨𝐴,
𝐴⟩, 𝐴⟩} ∈ GrpOp |