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

Metamath Proof Explorer

Theorem gidsn

Proof