This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mgm1

Description: The structure with one element and the only closed internal operation for a singleton is a magma. (Contributed by AV, 10-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 mgm1.m ⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ }
2 df-ov ⊢ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ )
3 opex ⊢ ⟨ 𝐼 , 𝐼 ⟩ ∈ V
4 fvsng ⊢ ( ( ⟨ 𝐼 , 𝐼 ⟩ ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ ) = 𝐼 )
5 3 4 mpan ⊢ ( 𝐼 ∈ 𝑉 → ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ ) = 𝐼 )
6 2 5 eqtrid ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 )
7 snidg ⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ { 𝐼 } )
8 6 7 eqeltrd ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) ∈ { 𝐼 } )
9 oveq1 ⊢ ( 𝑥 = 𝐼 → ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) )
10 9 eleq1d ⊢ ( 𝑥 = 𝐼 → ( ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) ∈ { 𝐼 } ↔ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) ∈ { 𝐼 } ) )
11 10 ralbidv ⊢ ( 𝑥 = 𝐼 → ( ∀ 𝑦 ∈ { 𝐼 } ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) ∈ { 𝐼 } ↔ ∀ 𝑦 ∈ { 𝐼 } ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) ∈ { 𝐼 } ) )
12 11 ralsng ⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑥 ∈ { 𝐼 } ∀ 𝑦 ∈ { 𝐼 } ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) ∈ { 𝐼 } ↔ ∀ 𝑦 ∈ { 𝐼 } ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) ∈ { 𝐼 } ) )
13 oveq2 ⊢ ( 𝑦 = 𝐼 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) )
14 13 eleq1d ⊢ ( 𝑦 = 𝐼 → ( ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) ∈ { 𝐼 } ↔ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) ∈ { 𝐼 } ) )
15 14 ralsng ⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑦 ∈ { 𝐼 } ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) ∈ { 𝐼 } ↔ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) ∈ { 𝐼 } ) )
16 12 15 bitrd ⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑥 ∈ { 𝐼 } ∀ 𝑦 ∈ { 𝐼 } ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) ∈ { 𝐼 } ↔ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) ∈ { 𝐼 } ) )
17 8 16 mpbird ⊢ ( 𝐼 ∈ 𝑉 → ∀ 𝑥 ∈ { 𝐼 } ∀ 𝑦 ∈ { 𝐼 } ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) ∈ { 𝐼 } )
18 snex ⊢ { 𝐼 } ∈ V
19 1 grpbase ⊢ ( { 𝐼 } ∈ V → { 𝐼 } = ( Base ‘ 𝑀 ) )
20 18 19 ax-mp ⊢ { 𝐼 } = ( Base ‘ 𝑀 )
21 snex ⊢ { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V
22 1 grpplusg ⊢ ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V → { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ 𝑀 ) )
23 21 22 ax-mp ⊢ { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ 𝑀 )
24 20 23 ismgmn0 ⊢ ( 𝐼 ∈ { 𝐼 } → ( 𝑀 ∈ Mgm ↔ ∀ 𝑥 ∈ { 𝐼 } ∀ 𝑦 ∈ { 𝐼 } ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) ∈ { 𝐼 } ) )
25 7 24 syl ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑥 ∈ { 𝐼 } ∀ 𝑦 ∈ { 𝐼 } ( 𝑥 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑦 ) ∈ { 𝐼 } ) )
26 17 25 mpbird ⊢ ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Mgm )