Theorem dfgrp3e 18590

Description: Alternate definition of a group as a set with a closed, associative operation, for which solutions 𝑥 and 𝑦 of the equations (𝑎 + 𝑥) = 𝑏 and (𝑥 + 𝑎) = 𝑏 exist. Exercise 1 of [Herstein] p. 57. (Contributed by NM, 5-Dec-2006.) (Revised by AV, 28-Aug-2021.)

Hypotheses

Ref	Expression
dfgrp3.b	⊢ 𝐵 = (Base‘𝐺)
dfgrp3.p	⊢ + = (+g‘𝐺)

Assertion

Ref	Expression
dfgrp3e	⊢ (𝐺 ∈ Grp ↔ (𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))))

Distinct variable groups:   𝐵,𝑙,𝑟,𝑥,𝑦,𝑧   𝐺,𝑙,𝑟,𝑥,𝑦,𝑧   + ,𝑙,𝑟,𝑥,𝑦,𝑧

Proof of Theorem dfgrp3e

Dummy variable 𝑎 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfgrp3.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
2		dfgrp3.p	. . 3 ⊢ + = (+g‘𝐺)
3	1, 2	dfgrp3 18589	. 2 ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)))
4		simp2 1135	. . . 4 ⊢ ((𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → 𝐵 ≠ ∅)
5		sgrpmgm 18295	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ Smgrp → 𝐺 ∈ Mgm)
6	5	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵) → 𝐺 ∈ Mgm)
7	6	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → 𝐺 ∈ Mgm)
8		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵)
9	8	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)
10		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵)
11	1, 2	mgmcl 18244	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Mgm ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
12	7, 9, 10, 11	syl3anc 1369	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
13	12	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → (𝑥 + 𝑦) ∈ 𝐵)
14	1, 2	sgrpass 18296	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
15	14	3anassrs 1358	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
16	15	ralrimiva 3107	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
17	16	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
18		simpr 484	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))
19	13, 17, 18	3jca 1126	. . . . . . . . 9 ⊢ ((((𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)))
20	19	ex 412	. . . . . . . 8 ⊢ (((𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ((∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦) → ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))))
21	20	ralimdva 3102	. . . . . . 7 ⊢ ((𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵) → (∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦) → ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))))
22	21	ralimdva 3102	. . . . . 6 ⊢ (𝐺 ∈ Smgrp → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))))
23	22	a1d 25	. . . . 5 ⊢ (𝐺 ∈ Smgrp → (𝐵 ≠ ∅ → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)))))
24	23	3imp 1109	. . . 4 ⊢ ((𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)))
25	4, 24	jca 511	. . 3 ⊢ ((𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → (𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))))
26		n0 4277	. . . . . 6 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑎 𝑎 ∈ 𝐵)
27		3simpa 1146	. . . . . . . . 9 ⊢ (((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))))
28	27	2ralimi 3087	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))))
29	1, 2	issgrpn0 18293	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐵 → (𝐺 ∈ Smgrp ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))))
30	28, 29	syl5ibr 245	. . . . . . 7 ⊢ (𝑎 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → 𝐺 ∈ Smgrp))
31	30	exlimiv 1934	. . . . . 6 ⊢ (∃𝑎 𝑎 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → 𝐺 ∈ Smgrp))
32	26, 31	sylbi 216	. . . . 5 ⊢ (𝐵 ≠ ∅ → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → 𝐺 ∈ Smgrp))
33	32	imp 406	. . . 4 ⊢ ((𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))) → 𝐺 ∈ Smgrp)
34		simpl 482	. . . 4 ⊢ ((𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))) → 𝐵 ≠ ∅)
35		simp3 1136	. . . . . 6 ⊢ (((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))
36	35	2ralimi 3087	. . . . 5 ⊢ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))
37	36	adantl 481	. . . 4 ⊢ ((𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))
38	33, 34, 37	3jca 1126	. . 3 ⊢ ((𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))) → (𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)))
39	25, 38	impbii 208	. 2 ⊢ ((𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) ↔ (𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))))
40	3, 39	bitri 274	1 ⊢ (𝐺 ∈ Grp ↔ (𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942  ∀wral 3063  ∃wrex 3064  ∅c0 4253  ‘cfv 6418  (class class class)co 7255  Basecbs 16840  +_gcplusg 16888  Mgmcmgm 18239  Smgrpcsgrp 18289  Grpcgrp 18492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-1st 7804  df-2nd 7805  df-0g 17069  df-mgm 18241  df-sgrp 18290  df-mnd 18301  df-grp 18495  df-minusg 18496  df-sbg 18497

This theorem is referenced by: (None)