Step |
Hyp |
Ref |
Expression |
1 |
|
ablsn.1 |
⊢ 𝐴 ∈ V |
2 |
1
|
grposnOLD |
⊢ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∈ GrpOp |
3 |
|
opex |
⊢ 〈 𝐴 , 𝐴 〉 ∈ V |
4 |
3
|
rnsnop |
⊢ ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } = { 𝐴 } |
5 |
4
|
eqcomi |
⊢ { 𝐴 } = ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } |
6 |
|
eqid |
⊢ ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) = ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) |
7 |
5 6
|
grpoidcl |
⊢ ( { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∈ GrpOp → ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) ∈ { 𝐴 } ) |
8 |
|
elsni |
⊢ ( ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) ∈ { 𝐴 } → ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) = 𝐴 ) |
9 |
2 7 8
|
mp2b |
⊢ ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) = 𝐴 |