Metamath Proof Explorer


Theorem gidsn

Description: Obsolete as of 23-Jan-2020. Use mnd1id instead. The identity element of the trivial group. (Contributed by FL, 21-Jun-2010) (Proof shortened by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis ablsn.1 𝐴 ∈ V
Assertion gidsn ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) = 𝐴

Proof

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 ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) = 𝐴