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 syl5eq ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 )
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 ‘ 𝑀 ) = 𝐼 )