frgpuplem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > frgpuplem		Structured version Visualization version Unicode version

Theorem frgpuplem 18185

Description: Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.)

**Hypotheses**
Ref	Expression
frgpup.b
frgpup.n
frgpup.t
frgpup.h
frgpup.i
frgpup.a
frgpup.w	Word
frgpup.r	~_FG

**Assertion**
Ref	Expression
frgpuplem	$/\$ _g _g

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem frgpuplem Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		frgpup.w	. . . . . . 7 Word
2		frgpup.r	. . . . . . 7 ~_FG
3	1, 2	efgval 18130	. . . . . 6 $/\$ splice $\$
4		coeq2 5280	. . . . . . . . . . . . 13
5	4	oveq2d 6666	. . . . . . . . . . . 12 _g _g
6		eqid 2622	. . . . . . . . . . . 12 _g _g _g _g
7	5, 6	eqer 7777	. . . . . . . . . . 11 _g _g
8	7	a1i 11	. . . . . . . . . 10 _g _g
9		ssv 3625	. . . . . . . . . . 11
10	9	a1i 11	. . . . . . . . . 10
11	8, 10	erinxp 7821	. . . . . . . . 9 _g _g
12		df-xp 5120	. . . . . . . . . . . . 13 $/\$
13	12	ineq1i 3810	. . . . . . . . . . . 12 _g _g $/\$ _g _g
14		incom 3805	. . . . . . . . . . . 12 _g _g _g _g
15		inopab 5252	. . . . . . . . . . . 12 $/\$ _g _g $/\$ $/\$ _g _g
16	13, 14, 15	3eqtr3i 2652	. . . . . . . . . . 11 _g _g $/\$ $/\$ _g _g
17		vex 3203	. . . . . . . . . . . . . 14
18		vex 3203	. . . . . . . . . . . . . 14
19	17, 18	prss 4351	. . . . . . . . . . . . 13 $/\$
20	19	anbi1i 731	. . . . . . . . . . . 12 $/\$ $/\$ _g _g $/\$ _g _g
21	20	opabbii 4717	. . . . . . . . . . 11 $/\$ $/\$ _g _g $/\$ _g _g
22	16, 21	eqtri 2644	. . . . . . . . . 10 _g _g $/\$ _g _g
23		ereq1 7749	. . . . . . . . . 10 _g _g $/\$ _g _g _g _g $/\$ _g _g
24	22, 23	ax-mp 5	. . . . . . . . 9 _g _g $/\$ _g _g
25	11, 24	sylib 208	. . . . . . . 8 $/\$ _g _g
26		simplrl 800	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
27		fviss 6256	. . . . . . . . . . . . . . . 16 Word Word
28	1, 27	eqsstri 3635	. . . . . . . . . . . . . . 15 Word
29	28, 26	sseldi 3601	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Word
30		opelxpi 5148	. . . . . . . . . . . . . . . 16 $/\$
31	30	adantl 482	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
32		simprl 794	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
33		2oconcl 7583	. . . . . . . . . . . . . . . . 17 $\$
34	33	ad2antll 765	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$
35		opelxpi 5148	. . . . . . . . . . . . . . . 16 $/\$ $\$ $\$
36	32, 34, 35	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$
37	31, 36	s2cld 13616	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$ Word
38		splcl 13503	. . . . . . . . . . . . . 14 Word $/\$ $\$ Word splice $\$ Word
39	29, 37, 38	syl2anc 693	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ splice $\$ Word
40	1	efgrcl 18128	. . . . . . . . . . . . . . 15 $/\$ Word
41	26, 40	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ Word
42	41	simprd 479	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ Word
43	39, 42	eleqtrrd 2704	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ splice $\$
44	26, 43	jca 554	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ splice $\$
45		swrdcl 13419	. . . . . . . . . . . . . . . . . 18 Word substr Word
46	29, 45	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ substr Word
47		frgpup.b	. . . . . . . . . . . . . . . . . . 19
48		frgpup.n	. . . . . . . . . . . . . . . . . . 19
49		frgpup.t	. . . . . . . . . . . . . . . . . . 19
50		frgpup.h	. . . . . . . . . . . . . . . . . . 19
51		frgpup.i	. . . . . . . . . . . . . . . . . . 19
52		frgpup.a	. . . . . . . . . . . . . . . . . . 19
53	47, 48, 49, 50, 51, 52	frgpuptf 18183	. . . . . . . . . . . . . . . . . 18
54	53	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
55		ccatco 13581	. . . . . . . . . . . . . . . . 17 substr Word $/\$ $\$ Word $/\$ substr ++ $\$ substr ++ $\$
56	46, 37, 54, 55	syl3anc 1326	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ substr ++ $\$ substr ++ $\$
57	56	oveq2d 6666	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ _g substr ++ $\$ _g substr ++ $\$
58	50	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
59		grpmnd 17429	. . . . . . . . . . . . . . . . 17
60	58, 59	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
61		wrdco 13577	. . . . . . . . . . . . . . . . 17 substr Word $/\$ substr Word
62	46, 54, 61	syl2anc 693	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ substr Word
63		wrdco 13577	. . . . . . . . . . . . . . . . 17 $\$ Word $/\$ $\$ Word
64	37, 54, 63	syl2anc 693	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$ Word
65		eqid 2622	. . . . . . . . . . . . . . . . 17
66	47, 65	gsumccat 17378	. . . . . . . . . . . . . . . 16 $/\$ substr Word $/\$ $\$ Word _g substr ++ $\$ _g substr _g $\$
67	60, 62, 64, 66	syl3anc 1326	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ _g substr ++ $\$ _g substr _g $\$
68	54, 31, 36	s2co 13665	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$ $\$
69		df-ov 6653	. . . . . . . . . . . . . . . . . . . . . 22
70	69	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
71		df-ov 6653	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
72		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$
73	72	efgmval 18125	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$ $\$
74	71, 73	syl5eqr 2670	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $\$
75	74	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $\$ $\$
76	75	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $\$ $\$
77	47, 48, 49, 50, 51, 52, 72	frgpuptinv 18184	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$
78	30, 77	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
79	78	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $\$
80	76, 79	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $\$
81	69	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . . 22
82	80, 81	syl6reqr 2675	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $\$
83	70, 82	s2eqd 13608	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$
84	68, 83	eqtr4d 2659	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$
85	84	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ _g $\$ _g
86		simprr 796	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
87	54, 32, 86	fovrnd 6806	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
88	47, 48	grpinvcl 17467	. . . . . . . . . . . . . . . . . . . 20 $/\$
89	58, 87, 88	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
90	47, 65	gsumws2 17379	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ _g
91	60, 87, 89, 90	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ _g
92		eqid 2622	. . . . . . . . . . . . . . . . . . . 20
93	47, 65, 92, 48	grprinv 17469	. . . . . . . . . . . . . . . . . . 19 $/\$
94	58, 87, 93	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
95	85, 91, 94	3eqtrd 2660	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ _g $\$
96	95	oveq2d 6666	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ _g substr _g $\$ _g substr
97	47	gsumwcl 17377	. . . . . . . . . . . . . . . . . 18 $/\$ substr Word _g substr
98	60, 62, 97	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ _g substr
99	47, 65, 92	grprid 17453	. . . . . . . . . . . . . . . . 17 $/\$ _g substr _g substr _g substr
100	58, 98, 99	syl2anc 693	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ _g substr _g substr
101	96, 100	eqtrd 2656	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ _g substr _g $\$ _g substr
102	57, 67, 101	3eqtrrd 2661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ _g substr _g substr ++ $\$
103	102	oveq1d 6665	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ _g substr _g substr _g substr ++ $\$ _g substr
104		swrdcl 13419	. . . . . . . . . . . . . . . 16 Word substr Word
105	29, 104	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ substr Word
106		wrdco 13577	. . . . . . . . . . . . . . 15 substr Word $/\$ substr Word
107	105, 54, 106	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ substr Word
108	47, 65	gsumccat 17378	. . . . . . . . . . . . . 14 $/\$ substr Word $/\$ substr Word _g substr ++ substr _g substr _g substr
109	60, 62, 107, 108	syl3anc 1326	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ _g substr ++ substr _g substr _g substr
110		ccatcl 13359	. . . . . . . . . . . . . . . 16 substr Word $/\$ $\$ Word substr ++ $\$ Word
111	46, 37, 110	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ substr ++ $\$ Word
112		wrdco 13577	. . . . . . . . . . . . . . 15 substr ++ $\$ Word $/\$ substr ++ $\$ Word
113	111, 54, 112	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ substr ++ $\$ Word
114	47, 65	gsumccat 17378	. . . . . . . . . . . . . 14 $/\$ substr ++ $\$ Word $/\$ substr Word _g substr ++ $\$ ++ substr _g substr ++ $\$ _g substr
115	60, 113, 107, 114	syl3anc 1326	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ _g substr ++ $\$ ++ substr _g substr ++ $\$ _g substr
116	103, 109, 115	3eqtr4d 2666	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ _g substr ++ substr _g substr ++ $\$ ++ substr
117		simplrr 801	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
118		elfzuz 12338	. . . . . . . . . . . . . . . . . 18
119		eluzfz1 12348	. . . . . . . . . . . . . . . . . 18
120	117, 118, 119	3syl 18	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
121		lencl 13324	. . . . . . . . . . . . . . . . . . . 20 Word
122	29, 121	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
123		nn0uz 11722	. . . . . . . . . . . . . . . . . . 19
124	122, 123	syl6eleq 2711	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
125		eluzfz2 12349	. . . . . . . . . . . . . . . . . 18
126	124, 125	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
127		ccatswrd 13456	. . . . . . . . . . . . . . . . 17 Word $/\$ $/\$ $/\$ substr ++ substr substr
128	29, 120, 117, 126, 127	syl13anc 1328	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
129		swrdid 13428	. . . . . . . . . . . . . . . . 17 Word substr
130	29, 129	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ substr
131	128, 130	eqtrd 2656	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ substr ++ substr
132	131	coeq2d 5284	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ substr ++ substr
133		ccatco 13581	. . . . . . . . . . . . . . 15 substr Word $/\$ substr Word $/\$ substr ++ substr substr ++ substr
134	46, 105, 54, 133	syl3anc 1326	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ substr ++ substr substr ++ substr
135	132, 134	eqtr3d 2658	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ substr ++ substr
136	135	oveq2d 6666	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ _g _g substr ++ substr
137		splval 13502	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ Word splice $\$ substr ++ $\$ ++ substr
138	26, 117, 117, 37, 137	syl13anc 1328	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ splice $\$ substr ++ $\$ ++ substr
139	138	coeq2d 5284	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ splice $\$ substr ++ $\$ ++ substr
140		ccatco 13581	. . . . . . . . . . . . . . 15 substr ++ $\$ Word $/\$ substr Word $/\$ substr ++ $\$ ++ substr substr ++ $\$ ++ substr
141	111, 105, 54, 140	syl3anc 1326	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ substr ++ $\$ ++ substr substr ++ $\$ ++ substr
142	139, 141	eqtrd 2656	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ splice $\$ substr ++ $\$ ++ substr
143	142	oveq2d 6666	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ _g splice $\$ _g substr ++ $\$ ++ substr
144	116, 136, 143	3eqtr4d 2666	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ _g _g splice $\$
145		vex 3203	. . . . . . . . . . . 12
146		ovex 6678	. . . . . . . . . . . 12 splice $\$
147		eleq1 2689	. . . . . . . . . . . . . . 15
148		eleq1 2689	. . . . . . . . . . . . . . 15 splice $\$ splice $\$
149	147, 148	bi2anan9 917	. . . . . . . . . . . . . 14 $/\$ splice $\$ $/\$ $/\$ splice $\$
150	19, 149	syl5bbr 274	. . . . . . . . . . . . 13 $/\$ splice $\$ $/\$ splice $\$
151		coeq2 5280	. . . . . . . . . . . . . . 15
152	151	oveq2d 6666	. . . . . . . . . . . . . 14 _g _g
153		coeq2 5280	. . . . . . . . . . . . . . 15 splice $\$ splice $\$
154	153	oveq2d 6666	. . . . . . . . . . . . . 14 splice $\$ _g _g splice $\$
155	152, 154	eqeqan12d 2638	. . . . . . . . . . . . 13 $/\$ splice $\$ _g _g _g _g splice $\$
156	150, 155	anbi12d 747	. . . . . . . . . . . 12 $/\$ splice $\$ $/\$ _g _g $/\$ splice $\$ $/\$ _g _g splice $\$
157		eqid 2622	. . . . . . . . . . . 12 $/\$ _g _g $/\$ _g _g
158	145, 146, 156, 157	braba 4992	. . . . . . . . . . 11 $/\$ _g _g splice $\$ $/\$ splice $\$ $/\$ _g _g splice $\$
159	44, 144, 158	sylanbrc 698	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ _g _g splice $\$
160	159	ralrimivva 2971	. . . . . . . . 9 $/\$ $/\$ $/\$ _g _g splice $\$
161	160	ralrimivva 2971	. . . . . . . 8 $/\$ _g _g splice $\$
162		fvex 6201	. . . . . . . . . . 11 Word
163	1, 162	eqeltri 2697	. . . . . . . . . 10
164		erex 7766	. . . . . . . . . 10 $/\$ _g _g $/\$ _g _g
165	25, 163, 164	mpisyl 21	. . . . . . . . 9 $/\$ _g _g
166		ereq1 7749	. . . . . . . . . . 11 $/\$ _g _g $/\$ _g _g
167		breq 4655	. . . . . . . . . . . . 13 $/\$ _g _g splice $\$ $/\$ _g _g splice $\$
168	167	2ralbidv 2989	. . . . . . . . . . . 12 $/\$ _g _g splice $\$ $/\$ _g _g splice $\$
169	168	2ralbidv 2989	. . . . . . . . . . 11 $/\$ _g _g splice $\$ $/\$ _g _g splice $\$
170	166, 169	anbi12d 747	. . . . . . . . . 10 $/\$ _g _g $/\$ splice $\$ $/\$ _g _g $/\$ $/\$ _g _g splice $\$
171	170	elabg 3351	. . . . . . . . 9 $/\$ _g _g $/\$ _g _g $/\$ splice $\$ $/\$ _g _g $/\$ $/\$ _g _g splice $\$
172	165, 171	syl 17	. . . . . . . 8 $/\$ _g _g $/\$ splice $\$ $/\$ _g _g $/\$ $/\$ _g _g splice $\$
173	25, 161, 172	mpbir2and 957	. . . . . . 7 $/\$ _g _g $/\$ splice $\$
174		intss1 4492	. . . . . . 7 $/\$ _g _g $/\$ splice $\$ $/\$ splice $\$ $/\$ _g _g
175	173, 174	syl 17	. . . . . 6 $/\$ splice $\$ $/\$ _g _g
176	3, 175	syl5eqss 3649	. . . . 5 $/\$ _g _g
177	176	ssbrd 4696	. . . 4 $/\$ _g _g
178	177	imp 445	. . 3 $/\$ $/\$ _g _g
179	1, 2	efger 18131	. . . . . 6
180		errel 7751	. . . . . 6
181	179, 180	mp1i 13	. . . . 5
182		brrelex12 5155	. . . . 5 $/\$ $/\$
183	181, 182	sylan 488	. . . 4 $/\$ $/\$
184		preq12 4270	. . . . . . 7 $/\$
185	184	sseq1d 3632	. . . . . 6 $/\$
186		coeq2 5280	. . . . . . . 8
187	186	oveq2d 6666	. . . . . . 7 _g _g
188		coeq2 5280	. . . . . . . 8
189	188	oveq2d 6666	. . . . . . 7 _g _g
190	187, 189	eqeqan12d 2638	. . . . . 6 $/\$ _g _g _g _g
191	185, 190	anbi12d 747	. . . . 5 $/\$ $/\$ _g _g $/\$ _g _g
192	191, 157	brabga 4989	. . . 4 $/\$ $/\$ _g _g $/\$ _g _g
193	183, 192	syl 17	. . 3 $/\$ $/\$ _g _g $/\$ _g _g
194	178, 193	mpbid 222	. 2 $/\$ $/\$ _g _g
195	194	simprd 479	1 $/\$ _g _g

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 196 $/\$ wa 384

wceq 1483

wcel 1990

cab 2608

wral 2912

cvv 3200 $\$ cdif 3571

cin 3573

wss 3574

c0 3915

cif 4086

cpr 4179

cop 4183

cotp 4185

cint 4475 class class class wbr 4653

copab 4712

cid 5023

cxp 5112

ccom 5118

wrel 5119

wf 5884

cfv 5888 (class class class)co 6650

cmpt2 6652

c1o 7553

c2o 7554

wer 7739

cc0 9936

cn0 11292

cuz 11687

cfz 12326

chash 13117 Word cword 13291 ++ cconcat 13293 substr csubstr 13295 splice csplice 13296

cs2 13586

cbs 15857

cplusg 15941

c0g 16100

_g cgsu 16101

cmnd 17294

cgrp 17422

cminusg 17423 ~_FG cefg 18119

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-ot 4186 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327 df-fzo 12466 df-seq 12802 df-hash 13118 df-word 13299 df-concat 13301 df-s1 13302 df-substr 13303 df-splice 13304 df-s2 13593 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-0g 16102 df-gsum 16103 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-grp 17425 df-minusg 17426 df-efg 18122

This theorem is referenced by: frgpupf 18186

W3C validator