Metamath Proof Explorer


Theorem mnd1id

Description: The singleton element of atrivial monoid is its identity element. (Contributed 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 syl5bi ( 𝐼𝑉 → ( 𝑎 ∈ { 𝐼 } → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑎 ) = 𝑎 ) )
21 20 imp ( ( 𝐼𝑉𝑎 ∈ { 𝐼 } ) → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑎 ) = 𝑎 )
22 oveq1 ( 𝑎 = 𝐼 → ( 𝑎 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) )
23 22 17 eqeq12d ( 𝑎 = 𝐼 → ( ( 𝑎 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝑎 ↔ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 ) )
24 15 23 syl5ibrcom ( 𝐼𝑉 → ( 𝑎 = 𝐼 → ( 𝑎 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝑎 ) )
25 10 24 syl5bi ( 𝐼𝑉 → ( 𝑎 ∈ { 𝐼 } → ( 𝑎 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝑎 ) )
26 25 imp ( ( 𝐼𝑉𝑎 ∈ { 𝐼 } ) → ( 𝑎 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝑎 )
27 4 5 8 9 21 26 ismgmid2 ( 𝐼𝑉𝐼 = ( 0g𝑀 ) )
28 27 eqcomd ( 𝐼𝑉 → ( 0g𝑀 ) = 𝐼 )