| Step | Hyp | Ref
| Expression |
| 1 | | snex 5436 |
. 2
⊢ {𝐴} ∈ V |
| 2 | | opex 5469 |
. . . . 5
⊢
〈𝐴, 𝐴〉 ∈ V |
| 3 | | grposnOLD.1 |
. . . . 5
⊢ 𝐴 ∈ V |
| 4 | 2, 3 | f1osn 6888 |
. . . 4
⊢
{〈〈𝐴,
𝐴〉, 𝐴〉}:{〈𝐴, 𝐴〉}–1-1-onto→{𝐴} |
| 5 | | f1of 6848 |
. . . 4
⊢
({〈〈𝐴,
𝐴〉, 𝐴〉}:{〈𝐴, 𝐴〉}–1-1-onto→{𝐴} → {〈〈𝐴, 𝐴〉, 𝐴〉}:{〈𝐴, 𝐴〉}⟶{𝐴}) |
| 6 | 4, 5 | ax-mp 5 |
. . 3
⊢
{〈〈𝐴,
𝐴〉, 𝐴〉}:{〈𝐴, 𝐴〉}⟶{𝐴} |
| 7 | 3, 3 | xpsn 7161 |
. . . 4
⊢ ({𝐴} × {𝐴}) = {〈𝐴, 𝐴〉} |
| 8 | 7 | feq2i 6728 |
. . 3
⊢
({〈〈𝐴,
𝐴〉, 𝐴〉}:({𝐴} × {𝐴})⟶{𝐴} ↔ {〈〈𝐴, 𝐴〉, 𝐴〉}:{〈𝐴, 𝐴〉}⟶{𝐴}) |
| 9 | 6, 8 | mpbir 231 |
. 2
⊢
{〈〈𝐴,
𝐴〉, 𝐴〉}:({𝐴} × {𝐴})⟶{𝐴} |
| 10 | | velsn 4642 |
. . 3
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
| 11 | | velsn 4642 |
. . 3
⊢ (𝑦 ∈ {𝐴} ↔ 𝑦 = 𝐴) |
| 12 | | velsn 4642 |
. . 3
⊢ (𝑧 ∈ {𝐴} ↔ 𝑧 = 𝐴) |
| 13 | | oveq2 7439 |
. . . . . 6
⊢ (𝑧 = 𝐴 → ((𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦){〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = ((𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦){〈〈𝐴, 𝐴〉, 𝐴〉}𝐴)) |
| 14 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦) = (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦)) |
| 15 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦) = (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝐴)) |
| 16 | | df-ov 7434 |
. . . . . . . . . . 11
⊢ (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝐴) = ({〈〈𝐴, 𝐴〉, 𝐴〉}‘〈𝐴, 𝐴〉) |
| 17 | 2, 3 | fvsn 7201 |
. . . . . . . . . . 11
⊢
({〈〈𝐴,
𝐴〉, 𝐴〉}‘〈𝐴, 𝐴〉) = 𝐴 |
| 18 | 16, 17 | eqtri 2765 |
. . . . . . . . . 10
⊢ (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝐴) = 𝐴 |
| 19 | 15, 18 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦) = 𝐴) |
| 20 | 14, 19 | sylan9eq 2797 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → (𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦) = 𝐴) |
| 21 | 20 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → ((𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦){〈〈𝐴, 𝐴〉, 𝐴〉}𝐴) = (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝐴)) |
| 22 | 21, 18 | eqtrdi 2793 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → ((𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦){〈〈𝐴, 𝐴〉, 𝐴〉}𝐴) = 𝐴) |
| 23 | 13, 22 | sylan9eqr 2799 |
. . . . 5
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) ∧ 𝑧 = 𝐴) → ((𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦){〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = 𝐴) |
| 24 | 23 | 3impa 1110 |
. . . 4
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → ((𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦){〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = 𝐴) |
| 25 | | oveq1 7438 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥{〈〈𝐴, 𝐴〉, 𝐴〉} (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧)) = (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉} (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧))) |
| 26 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧)) |
| 27 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐴 → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝐴)) |
| 28 | 27, 18 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑧 = 𝐴 → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = 𝐴) |
| 29 | 26, 28 | sylan9eq 2797 |
. . . . . . . 8
⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = 𝐴) |
| 30 | 29 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉} (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧)) = (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝐴)) |
| 31 | 30, 18 | eqtrdi 2793 |
. . . . . 6
⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉} (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧)) = 𝐴) |
| 32 | 25, 31 | sylan9eq 2797 |
. . . . 5
⊢ ((𝑥 = 𝐴 ∧ (𝑦 = 𝐴 ∧ 𝑧 = 𝐴)) → (𝑥{〈〈𝐴, 𝐴〉, 𝐴〉} (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧)) = 𝐴) |
| 33 | 32 | 3impb 1115 |
. . . 4
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → (𝑥{〈〈𝐴, 𝐴〉, 𝐴〉} (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧)) = 𝐴) |
| 34 | 24, 33 | eqtr4d 2780 |
. . 3
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ∧ 𝑧 = 𝐴) → ((𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦){〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = (𝑥{〈〈𝐴, 𝐴〉, 𝐴〉} (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧))) |
| 35 | 10, 11, 12, 34 | syl3anb 1162 |
. 2
⊢ ((𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴} ∧ 𝑧 ∈ {𝐴}) → ((𝑥{〈〈𝐴, 𝐴〉, 𝐴〉}𝑦){〈〈𝐴, 𝐴〉, 𝐴〉}𝑧) = (𝑥{〈〈𝐴, 𝐴〉, 𝐴〉} (𝑦{〈〈𝐴, 𝐴〉, 𝐴〉}𝑧))) |
| 36 | 3 | snid 4662 |
. 2
⊢ 𝐴 ∈ {𝐴} |
| 37 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑥) = (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝐴)) |
| 38 | 37, 18 | eqtrdi 2793 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑥) = 𝐴) |
| 39 | | id 22 |
. . . 4
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) |
| 40 | 38, 39 | eqtr4d 2780 |
. . 3
⊢ (𝑥 = 𝐴 → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑥) = 𝑥) |
| 41 | 10, 40 | sylbi 217 |
. 2
⊢ (𝑥 ∈ {𝐴} → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑥) = 𝑥) |
| 42 | 36 | a1i 11 |
. 2
⊢ (𝑥 ∈ {𝐴} → 𝐴 ∈ {𝐴}) |
| 43 | 10, 38 | sylbi 217 |
. 2
⊢ (𝑥 ∈ {𝐴} → (𝐴{〈〈𝐴, 𝐴〉, 𝐴〉}𝑥) = 𝐴) |
| 44 | 1, 9, 35, 36, 41, 42, 43 | isgrpoi 30517 |
1
⊢
{〈〈𝐴,
𝐴〉, 𝐴〉} ∈ GrpOp |