Step | Hyp | Ref
| Expression |
1 | | snex 5324 |
. 2
⊢ {𝐴} ∈ V |
2 | | opex 5348 |
. . . . 5
⊢
〈𝐴, 𝐴〉 ∈ V |
3 | | grposnOLD.1 |
. . . . 5
⊢ 𝐴 ∈ V |
4 | 2, 3 | f1osn 6700 |
. . . 4
⊢
{〈〈𝐴,
𝐴〉, 𝐴〉}:{〈𝐴, 𝐴〉}–1-1-onto→{𝐴} |
5 | | f1of 6661 |
. . . 4
⊢
({〈〈𝐴,
𝐴〉, 𝐴〉}:{〈𝐴, 𝐴〉}–1-1-onto→{𝐴} → {〈〈𝐴, 𝐴〉, 𝐴〉}:{〈𝐴, 𝐴〉}⟶{𝐴}) |
6 | 4, 5 | ax-mp 5 |
. . 3
⊢
{〈〈𝐴,
𝐴〉, 𝐴〉}:{〈𝐴, 𝐴〉}⟶{𝐴} |
7 | 3, 3 | xpsn 6956 |
. . . 4
⊢ ({𝐴} × {𝐴}) = {〈𝐴, 𝐴〉} |
8 | 7 | feq2i 6537 |
. . 3
⊢
({〈〈𝐴,
𝐴〉, 𝐴〉}:({𝐴} × {𝐴})⟶{𝐴} ↔ {〈〈𝐴, 𝐴〉, 𝐴〉}:{〈𝐴, 𝐴〉}⟶{𝐴}) |
9 | 6, 8 | mpbir 234 |
. 2
⊢
{〈〈𝐴,
𝐴〉, 𝐴〉}:({𝐴} × {𝐴})⟶{𝐴} |
10 | | velsn 4557 |
. . 3
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
11 | | velsn 4557 |
. . 3
⊢ (𝑦 ∈ {𝐴} ↔ 𝑦 = 𝐴) |
12 | | velsn 4557 |
. . 3
⊢ (𝑧 ∈ {𝐴} ↔ 𝑧 = 𝐴) |
13 | | oveq2 7221 |
. . . . . 6
⊢ (𝑧 = 𝐴 → ((𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦){〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = ((𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦){〈〈𝐴, 𝐴〉, 𝐴〉}𝐴)) |
14 | | oveq1 7220 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦) = (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦)) |
15 | | oveq2 7221 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦) = (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝐴)) |
16 | | df-ov 7216 |
. . . . . . . . . . 11
⊢ (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝐴) = ({〈〈𝐴, 𝐴〉, 𝐴〉}‘〈𝐴, 𝐴〉) |
17 | 2, 3 | fvsn 6996 |
. . . . . . . . . . 11
⊢
({〈〈𝐴,
𝐴〉, 𝐴〉}‘〈𝐴, 𝐴〉) = 𝐴 |
18 | 16, 17 | eqtri 2765 |
. . . . . . . . . 10
⊢ (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝐴) = 𝐴 |
19 | 15, 18 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦) = 𝐴) |
20 | 14, 19 | sylan9eq 2798 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → (𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦) = 𝐴) |
21 | 20 | oveq1d 7228 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → ((𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦){〈〈𝐴, 𝐴〉, 𝐴〉}𝐴) = (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝐴)) |
22 | 21, 18 | eqtrdi 2794 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → ((𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦){〈〈𝐴, 𝐴〉, 𝐴〉}𝐴) = 𝐴) |
23 | 13, 22 | sylan9eqr 2800 |
. . . . 5
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) ∧ 𝑧 = 𝐴) → ((𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦){〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = 𝐴) |
24 | 23 | 3impa 1112 |
. . . 4
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → ((𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦){〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = 𝐴) |
25 | | oveq1 7220 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥{〈〈𝐴, 𝐴〉, 𝐴〉} (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧)) = (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉} (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧))) |
26 | | oveq1 7220 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧)) |
27 | | oveq2 7221 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐴 → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝐴)) |
28 | 27, 18 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝑧 = 𝐴 → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = 𝐴) |
29 | 26, 28 | sylan9eq 2798 |
. . . . . . . 8
⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = 𝐴) |
30 | 29 | oveq2d 7229 |
. . . . . . 7
⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉} (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧)) = (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝐴)) |
31 | 30, 18 | eqtrdi 2794 |
. . . . . 6
⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉} (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧)) = 𝐴) |
32 | 25, 31 | sylan9eq 2798 |
. . . . 5
⊢ ((𝑥 = 𝐴 ∧ (𝑦 = 𝐴 ∧ 𝑧 = 𝐴)) → (𝑥{〈〈𝐴, 𝐴〉, 𝐴〉} (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧)) = 𝐴) |
33 | 32 | 3impb 1117 |
. . . 4
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → (𝑥{〈〈𝐴, 𝐴〉, 𝐴〉} (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧)) = 𝐴) |
34 | 24, 33 | eqtr4d 2780 |
. . 3
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → ((𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦){〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = (𝑥{〈〈𝐴, 𝐴〉, 𝐴〉} (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧))) |
35 | 10, 11, 12, 34 | syl3anb 1163 |
. 2
⊢ ((𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴} ∧ 𝑧 ∈ {𝐴}) → ((𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦){〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = (𝑥{〈〈𝐴, 𝐴〉, 𝐴〉} (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧))) |
36 | 3 | snid 4577 |
. 2
⊢ 𝐴 ∈ {𝐴} |
37 | | oveq2 7221 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑥) = (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝐴)) |
38 | 37, 18 | eqtrdi 2794 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑥) = 𝐴) |
39 | | id 22 |
. . . 4
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) |
40 | 38, 39 | eqtr4d 2780 |
. . 3
⊢ (𝑥 = 𝐴 → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑥) = 𝑥) |
41 | 10, 40 | sylbi 220 |
. 2
⊢ (𝑥 ∈ {𝐴} → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑥) = 𝑥) |
42 | 36 | a1i 11 |
. 2
⊢ (𝑥 ∈ {𝐴} → 𝐴 ∈ {𝐴}) |
43 | 10, 38 | sylbi 220 |
. 2
⊢ (𝑥 ∈ {𝐴} → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑥) = 𝐴) |
44 | 1, 9, 35, 36, 41, 42, 43 | isgrpoi 28579 |
1
⊢
{〈〈𝐴,
𝐴〉, 𝐴〉} ∈ GrpOp |