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	$⊢ A \in V$
	Assertion	gidsn	$⊢ GId (\{⟨⟨A, A⟩, A⟩\}) = A$

Proof

Step	Hyp	Ref	Expression
1		ablsn.1	$⊢ A \in V$
2	1	grposnOLD	$⊢ \{⟨⟨A, A⟩, A⟩\} \in GrpOp$
3		opex	$⊢ ⟨A, A⟩ \in V$
4	3	rnsnop	$⊢ ran \{⟨⟨A, A⟩, A⟩\} = \{A\}$
5	4	eqcomi	$⊢ \{A\} = ran \{⟨⟨A, A⟩, A⟩\}$
6		eqid	$⊢ GId (\{⟨⟨A, A⟩, A⟩\}) = GId (\{⟨⟨A, A⟩, A⟩\})$
7	5 6	grpoidcl	$⊢ \{⟨⟨A, A⟩, A⟩\} \in GrpOp \to GId (\{⟨⟨A, A⟩, A⟩\}) \in \{A\}$
8		elsni	$⊢ GId (\{⟨⟨A, A⟩, A⟩\}) \in \{A\} \to GId (\{⟨⟨A, A⟩, A⟩\}) = A$
9	2 7 8	mp2b	$⊢ GId (\{⟨⟨A, A⟩, A⟩\}) = A$

Metamath Proof Explorer

Theorem gidsn

Proof