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