Theorem mnd1id

Description: The singleton element of atrivial monoid is its identity element. (Contributed by FL, 21-Jun-2010) (Revised by AV, 23-Jan-2020)

	Ref	Expression
Hypothesis	mnd1.m	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ }
Assertion	mnd1id	⊢ ( 𝐼 ∈ 𝑉 → ( 0g ‘ 𝑀 ) = 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		mnd1.m	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ }
2		snex	⊢ { 𝐼 } ∈ V
3	1	grpbase	⊢ ( { 𝐼 } ∈ V → { 𝐼 } = ( Base ‘ 𝑀 ) )
4	2 3	ax-mp	⊢ { 𝐼 } = ( Base ‘ 𝑀 )
5		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
6		snex	⊢ { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V
7	1	grpplusg	⊢ ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V → { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ 𝑀 ) )
8	6 7	ax-mp	⊢ { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ 𝑀 )
9		snidg	⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ { 𝐼 } )
10		velsn	⊢ ( 𝑎 ∈ { 𝐼 } ↔ 𝑎 = 𝐼 )
11		df-ov	⊢ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ )
12		opex	⊢ ⟨ 𝐼 , 𝐼 ⟩ ∈ V
13		fvsng	⊢ ( ( ⟨ 𝐼 , 𝐼 ⟩ ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ ) = 𝐼 )
14	12 13	mpan	⊢ ( 𝐼 ∈ 𝑉 → ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ ) = 𝐼 )
15	11 14	eqtrid	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 )
16		oveq2	⊢ ( 𝑎 = 𝐼 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑎 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) )
17		id	⊢ ( 𝑎 = 𝐼 → 𝑎 = 𝐼 )
18	16 17	eqeq12d	⊢ ( 𝑎 = 𝐼 → ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑎 ) = 𝑎 ↔ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 ) )
19	15 18	syl5ibrcom	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑎 = 𝐼 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑎 ) = 𝑎 ) )
20	10 19	biimtrid	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑎 ∈ { 𝐼 } → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑎 ) = 𝑎 ) )
21	20	imp	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑎 ∈ { 𝐼 } ) → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑎 ) = 𝑎 )
22		oveq1	⊢ ( 𝑎 = 𝐼 → ( 𝑎 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) )
23	22 17	eqeq12d	⊢ ( 𝑎 = 𝐼 → ( ( 𝑎 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝑎 ↔ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 ) )
24	15 23	syl5ibrcom	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑎 = 𝐼 → ( 𝑎 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝑎 ) )
25	10 24	biimtrid	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑎 ∈ { 𝐼 } → ( 𝑎 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝑎 ) )
26	25	imp	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑎 ∈ { 𝐼 } ) → ( 𝑎 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝑎 )
27	4 5 8 9 21 26	ismgmid2	⊢ ( 𝐼 ∈ 𝑉 → 𝐼 = ( 0g ‘ 𝑀 ) )
28	27	eqcomd	⊢ ( 𝐼 ∈ 𝑉 → ( 0g ‘ 𝑀 ) = 𝐼 )