Theorem issgrpv 17639

Description: The predicate "is a semigroup" for a structure which is a set. (Contributed by AV, 1-Feb-2020.)

Hypotheses

Ref	Expression
issgrpn0.b	⊢ 𝐵 = (Base‘𝑀)
issgrpn0.o	⊢ ⚬ = (+g‘𝑀)

Assertion

Ref	Expression
issgrpv	⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ SGrp ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))))

Distinct variable groups:   𝑥,𝐵,𝑦,𝑧   𝑥,𝑀,𝑦,𝑧   𝑥, ⚬ ,𝑦,𝑧

Allowed substitution hints:   𝑉(𝑥,𝑦,𝑧)

Proof of Theorem issgrpv

Step	Hyp	Ref	Expression
1		issgrpn0.b	. . . 4 ⊢ 𝐵 = (Base‘𝑀)
2		issgrpn0.o	. . . 4 ⊢ ⚬ = (+g‘𝑀)
3	1, 2	ismgm 17596	. . 3 ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ Mgm ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵))
4	3	anbi1d 625	. 2 ⊢ (𝑀 ∈ 𝑉 → ((𝑀 ∈ Mgm ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))) ↔ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))))
5	1, 2	issgrp 17638	. 2 ⊢ (𝑀 ∈ SGrp ↔ (𝑀 ∈ Mgm ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))
6		r19.26-2 3275	. 2 ⊢ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))) ↔ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))
7	4, 5, 6	3bitr4g 306	1 ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ SGrp ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1658   ∈ wcel 2166  ∀wral 3117  ‘cfv 6123  (class class class)co 6905  Basecbs 16222  +_gcplusg 16305  Mgmcmgm 17593  SGrpcsgrp 17636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-nul 5013

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-iota 6086  df-fv 6131  df-ov 6908  df-mgm 17595  df-sgrp 17637

This theorem is referenced by:  ismnd  17650  dfgrp2e  17802