Theorem grp1

Description: The (smallest) structure representing atrivial group. According to Wikipedia ("Trivial group", 28-Apr-2019, https://en.wikipedia.org/wiki/Trivial_group ) "In mathematics, a trivial group is a group consisting of a single element. All such groups are isomorphic, so one often speaks ofthe trivial group. The single element of the trivial group is the identity element". (Contributed by NM, 4-Nov-2006) (Revised by AV, 28-Apr-2019)

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

Proof

Step	Hyp	Ref	Expression
1		grp1.m	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ }
2	1	mnd1	⊢ ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd )
3		df-ov	⊢ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ )
4		opex	⊢ ⟨ 𝐼 , 𝐼 ⟩ ∈ V
5		fvsng	⊢ ( ( ⟨ 𝐼 , 𝐼 ⟩ ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ ) = 𝐼 )
6	4 5	mpan	⊢ ( 𝐼 ∈ 𝑉 → ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ ) = 𝐼 )
7	3 6	eqtrid	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 )
8	1	mnd1id	⊢ ( 𝐼 ∈ 𝑉 → ( 0g ‘ 𝑀 ) = 𝐼 )
9	7 8	eqtr4d	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) )
10		oveq2	⊢ ( 𝑖 = 𝐼 → ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑖 ) = ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) )
11	10	eqeq1d	⊢ ( 𝑖 = 𝐼 → ( ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑖 ) = ( 0g ‘ 𝑀 ) ↔ ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) ) )
12	11	rexbidv	⊢ ( 𝑖 = 𝐼 → ( ∃ 𝑒 ∈ { 𝐼 } ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑖 ) = ( 0g ‘ 𝑀 ) ↔ ∃ 𝑒 ∈ { 𝐼 } ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) ) )
13	12	ralsng	⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑖 ∈ { 𝐼 } ∃ 𝑒 ∈ { 𝐼 } ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑖 ) = ( 0g ‘ 𝑀 ) ↔ ∃ 𝑒 ∈ { 𝐼 } ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) ) )
14		oveq1	⊢ ( 𝑒 = 𝐼 → ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) )
15	14	eqeq1d	⊢ ( 𝑒 = 𝐼 → ( ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) ↔ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) ) )
16	15	rexsng	⊢ ( 𝐼 ∈ 𝑉 → ( ∃ 𝑒 ∈ { 𝐼 } ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) ↔ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) ) )
17	13 16	bitrd	⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑖 ∈ { 𝐼 } ∃ 𝑒 ∈ { 𝐼 } ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑖 ) = ( 0g ‘ 𝑀 ) ↔ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) ) )
18	9 17	mpbird	⊢ ( 𝐼 ∈ 𝑉 → ∀ 𝑖 ∈ { 𝐼 } ∃ 𝑒 ∈ { 𝐼 } ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑖 ) = ( 0g ‘ 𝑀 ) )
19		snex	⊢ { 𝐼 } ∈ V
20	1	grpbase	⊢ ( { 𝐼 } ∈ V → { 𝐼 } = ( Base ‘ 𝑀 ) )
21	19 20	ax-mp	⊢ { 𝐼 } = ( Base ‘ 𝑀 )
22		snex	⊢ { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V
23	1	grpplusg	⊢ ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V → { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ 𝑀 ) )
24	22 23	ax-mp	⊢ { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ 𝑀 )
25		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
26	21 24 25	isgrp	⊢ ( 𝑀 ∈ Grp ↔ ( 𝑀 ∈ Mnd ∧ ∀ 𝑖 ∈ { 𝐼 } ∃ 𝑒 ∈ { 𝐼 } ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑖 ) = ( 0g ‘ 𝑀 ) ) )
27	2 18 26	sylanbrc	⊢ ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Grp )