Metamath Proof Explorer

Theorem mnd1

Description: The (smallest) structure representing atrivial monoid consists of one element. (Contributed by AV, 28-Apr-2019) (Proof shortened by AV, 11-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 mnd1.m ⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ }
2 1 sgrp1 ⊢ ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Smgrp )
3 df-ov ⊢ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ )
4 opex ⊢ ⟨ 𝐼 , 𝐼 ⟩ ∈ V
5 fvsng ⊢ ( ( ⟨ 𝐼 , 𝐼 ⟩ ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ ) = 𝐼 )
6 4 5 mpan ⊢ ( 𝐼 ∈ 𝑉 → ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ ) = 𝐼 )
7 3 6 syl5eq ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 )
8 oveq2 ⊢ ( 𝑦 = 𝐼 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) )
9 id ⊢ ( 𝑦 = 𝐼 → 𝑦 = 𝐼 )
10 8 9 eqeq12d ⊢ ( 𝑦 = 𝐼 → ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = 𝑦 ↔ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 ) )
11 oveq1 ⊢ ( 𝑦 = 𝐼 → ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) )
12 11 9 eqeq12d ⊢ ( 𝑦 = 𝐼 → ( ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝑦 ↔ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 ) )
13 10 12 anbi12d ⊢ ( 𝑦 = 𝐼 → ( ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = 𝑦 ∧ ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝑦 ) ↔ ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 ∧ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 ) ) )
14 13 ralsng ⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑦 ∈ { 𝐼 } ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = 𝑦 ∧ ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝑦 ) ↔ ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 ∧ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 ) ) )
15 7 7 14 mpbir2and ⊢ ( 𝐼 ∈ 𝑉 → ∀ 𝑦 ∈ { 𝐼 } ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = 𝑦 ∧ ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝑦 ) )
16 oveq1 ⊢ ( 𝑥 = 𝐼 → ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) )
17 16 eqeq1d ⊢ ( 𝑥 = 𝐼 → ( ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = 𝑦 ↔ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = 𝑦 ) )
18 17 ovanraleqv ⊢ ( 𝑥 = 𝐼 → ( ∀ 𝑦 ∈ { 𝐼 } ( ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = 𝑦 ∧ ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ { 𝐼 } ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = 𝑦 ∧ ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝑦 ) ) )
19 18 rexsng ⊢ ( 𝐼 ∈ 𝑉 → ( ∃ 𝑥 ∈ { 𝐼 } ∀ 𝑦 ∈ { 𝐼 } ( ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = 𝑦 ∧ ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ { 𝐼 } ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = 𝑦 ∧ ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝑦 ) ) )
20 15 19 mpbird ⊢ ( 𝐼 ∈ 𝑉 → ∃ 𝑥 ∈ { 𝐼 } ∀ 𝑦 ∈ { 𝐼 } ( ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = 𝑦 ∧ ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑥 ) = 𝑦 ) )
21 snex ⊢ { 𝐼 } ∈ V
22 1 grpbase ⊢ ( { 𝐼 } ∈ V → { 𝐼 } = ( Base ‘ 𝑀 ) )
23 21 22 ax-mp ⊢ { 𝐼 } = ( Base ‘ 𝑀 )
24 snex ⊢ { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V
25 1 grpplusg ⊢ ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V → { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ 𝑀 ) )
26 24 25 ax-mp ⊢ { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ 𝑀 )
27 23 26 ismnddef ⊢ ( 𝑀 ∈ Mnd ↔ ( 𝑀 ∈ Smgrp ∧ ∃ 𝑥 ∈ { 𝐼 } ∀ 𝑦 ∈ { 𝐼 } ( ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = 𝑦 ∧ ( 𝑦 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑥 ) = 𝑦 ) ) )
28 2 20 27 sylanbrc ⊢ ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd )