mdetunilem9 - Metamath Proof Explorer

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

Theorem mdetunilem9 20426

Description: Lemma for mdetuni 20428. (Contributed by SO, 15-Jul-2018.)

**Hypotheses**
Ref	Expression
mdetuni.a	Mat
mdetuni.b
mdetuni.k
mdetuni.0g
mdetuni.1r
mdetuni.pg
mdetuni.tg
mdetuni.n
mdetuni.r
mdetuni.ff
mdetuni.al	$/\$
mdetuni.li	$/\$ $\$ $\$ $/\$ $\$ $\$
mdetuni.sc	$/\$ $\$ $\$
mdetunilem9.id
mdetunilem9.y

**Assertion**
Ref	Expression
mdetunilem9

Distinct variable groups:

Allowed substitution hints:

(

)

Proof of Theorem mdetunilem9 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ral0 4076	. . . 4
2		simpr 477	. . . . 5 $/\$
3		f1oi 6174	. . . . . . . 8
4		f1of 6137	. . . . . . . 8
5	3, 4	mp1i 13	. . . . . . 7
6		mdetuni.n	. . . . . . . 8
7	6, 6	elmapd 7871	. . . . . . 7
8	5, 7	mpbird 247	. . . . . 6
9	8	adantr 481	. . . . 5 $/\$
10		simplrl 800	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
11		mdetuni.a	. . . . . . . . . . . . . . . . 17 Mat
12		mdetuni.k	. . . . . . . . . . . . . . . . 17
13		mdetuni.b	. . . . . . . . . . . . . . . . 17
14	11, 12, 13	matbas2i 20228	. . . . . . . . . . . . . . . 16
15		elmapi 7879	. . . . . . . . . . . . . . . 16
16	14, 15	syl 17	. . . . . . . . . . . . . . 15
17	16	feqmptd 6249	. . . . . . . . . . . . . 14
18	17	fveq2d 6195	. . . . . . . . . . . . 13
19	10, 18	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
20		eqid 2622	. . . . . . . . . . . . . 14
21		mpteq12 4736	. . . . . . . . . . . . . . 15 $/\$
22	21	fveq2d 6195	. . . . . . . . . . . . . 14 $/\$
23	20, 22	mpan 706	. . . . . . . . . . . . 13
24	23	adantl 482	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
25		eleq1 2689	. . . . . . . . . . . . . . . . 17
26	25	anbi2d 740	. . . . . . . . . . . . . . . 16 $/\$ $/\$
27		elequ2 2004	. . . . . . . . . . . . . . . . . . . 20
28	27	ifbid 4108	. . . . . . . . . . . . . . . . . . 19
29	28	mpteq2dv 4745	. . . . . . . . . . . . . . . . . 18
30	29	fveq2d 6195	. . . . . . . . . . . . . . . . 17
31	30	eqeq1d 2624	. . . . . . . . . . . . . . . 16
32	26, 31	imbi12d 334	. . . . . . . . . . . . . . 15 $/\$ $/\$
33		eleq1 2689	. . . . . . . . . . . . . . . . . . . 20
34	33	ifbid 4108	. . . . . . . . . . . . . . . . . . 19
35	34	mpt2mpt 6752	. . . . . . . . . . . . . . . . . 18
36		elmapi 7879	. . . . . . . . . . . . . . . . . . . . . . . . 25
37	36	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
38		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . 24
39	37, 38	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
40	39	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
41		simp2 1062	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
42		fnopfvb 6237	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
43	40, 41, 42	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
44	43	bicomd 213	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
45	44	ifbid 4108	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
46	45	mpt2eq3dva 6719	. . . . . . . . . . . . . . . . . 18 $/\$
47	35, 46	syl5eq 2668	. . . . . . . . . . . . . . . . 17 $/\$
48	47	fveq2d 6195	. . . . . . . . . . . . . . . 16 $/\$
49		mdetuni.0g	. . . . . . . . . . . . . . . . . 18
50		mdetuni.1r	. . . . . . . . . . . . . . . . . 18
51		mdetuni.pg	. . . . . . . . . . . . . . . . . 18
52		mdetuni.tg	. . . . . . . . . . . . . . . . . 18
53		mdetuni.r	. . . . . . . . . . . . . . . . . 18
54		mdetuni.ff	. . . . . . . . . . . . . . . . . 18
55		mdetuni.al	. . . . . . . . . . . . . . . . . 18 $/\$
56		mdetuni.li	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$ $/\$ $\$ $\$
57		mdetuni.sc	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$
58		mdetunilem9.id	. . . . . . . . . . . . . . . . . 18
59	11, 13, 12, 49, 50, 51, 52, 6, 53, 54, 55, 56, 57, 58	mdetunilem8 20425	. . . . . . . . . . . . . . . . 17 $/\$
60	36, 59	sylan2 491	. . . . . . . . . . . . . . . 16 $/\$
61	48, 60	eqtrd 2656	. . . . . . . . . . . . . . 15 $/\$
62	32, 61	chvarv 2263	. . . . . . . . . . . . . 14 $/\$
63	62	adantrl 752	. . . . . . . . . . . . 13 $/\$ $/\$
64	63	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
65	19, 24, 64	3eqtrd 2660	. . . . . . . . . . 11 $/\$ $/\$ $/\$
66	65	ex 450	. . . . . . . . . 10 $/\$ $/\$
67	66	ralrimivva 2971	. . . . . . . . 9
68		xpfi 8231	. . . . . . . . . . 11 $/\$
69	6, 6, 68	syl2anc 693	. . . . . . . . . 10
70		raleq 3138	. . . . . . . . . . . . 13
71	70	imbi1d 331	. . . . . . . . . . . 12
72	71	2ralbidv 2989	. . . . . . . . . . 11
73		mdetunilem9.y	. . . . . . . . . . 11
74	72, 73	elab2g 3353	. . . . . . . . . 10
75	69, 74	syl 17	. . . . . . . . 9
76	67, 75	mpbird 247	. . . . . . . 8
77		ssid 3624	. . . . . . . . 9
78	69	3ad2ant1 1082	. . . . . . . . . . 11 $/\$ $/\$
79		sseq1 3626	. . . . . . . . . . . . . 14
80	79	3anbi2d 1404	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
81		eleq1 2689	. . . . . . . . . . . . . 14
82	81	notbid 308	. . . . . . . . . . . . 13
83	80, 82	imbi12d 334	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
84		sseq1 3626	. . . . . . . . . . . . . 14
85	84	3anbi2d 1404	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
86		eleq1 2689	. . . . . . . . . . . . . 14
87	86	notbid 308	. . . . . . . . . . . . 13
88	85, 87	imbi12d 334	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
89		sseq1 3626	. . . . . . . . . . . . . 14
90	89	3anbi2d 1404	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
91		eleq1 2689	. . . . . . . . . . . . . 14
92	91	notbid 308	. . . . . . . . . . . . 13
93	90, 92	imbi12d 334	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
94		sseq1 3626	. . . . . . . . . . . . . 14
95	94	3anbi2d 1404	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
96		eleq1 2689	. . . . . . . . . . . . . 14
97	96	notbid 308	. . . . . . . . . . . . 13
98	95, 97	imbi12d 334	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
99		simp3 1063	. . . . . . . . . . . 12 $/\$ $/\$
100		ssun1 3776	. . . . . . . . . . . . . . . 16
101		sstr2 3610	. . . . . . . . . . . . . . . 16
102	100, 101	ax-mp 5	. . . . . . . . . . . . . . 15
103	102	3anim2i 1249	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
104	103	imim1i 63	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
105		simpl1 1064	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
106		simpl2 1065	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
107		simprll 802	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
108	11, 12, 13	matbas2i 20228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
109		elmapi 7879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
110	108, 109	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
111	110	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
112	111	feqmptd 6249	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
113	112	reseq1d 5395	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
114	53	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
115		ringgrp 18552	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
116	114, 115	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
117	116	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
118	111	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
119		simp2 1062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$
120	119	unssbd 3791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
121		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
122	121	snss 4316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
123	120, 122	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
124		xp1st 7198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
125	123, 124	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$
126	125	snssd 4340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
127		xpss1 5228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
128	126, 127	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
129	128	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
130	118, 129	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
131	12, 50	ringidcl 18568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
132	114, 131	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
133	12, 49	ring0cl 18569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
134	114, 133	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
135	132, 134	ifcld 4131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
136	135	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
137		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
138	12, 51, 137	grpnpcan 17507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
139	117, 130, 136, 138	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
140	139	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
141	140	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
142		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
143		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
144	142, 143	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
145	144	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
146	141, 145	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
147	12, 51, 49	grplid 17452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
148	117, 130, 147	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
149	148	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
150	149	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
151		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
152		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
153	151, 152	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
154	153	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
155	150, 154	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
156	146, 155	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
157	156	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
158		snfi 8038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
159	6	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
160		xpfi 8231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
161	158, 159, 160	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
162		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
163		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
164	49, 163	eqeltri 2697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
165	162, 164	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
166	165	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
167		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
168	50, 167	eqeltri 2697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
169	168, 164	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
170		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
171	169, 170	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
173		xp1st 7198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
174		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
175		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
176	173, 174, 175	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
177	176	mpteq2ia 4740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
178	177	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
179		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
180	161, 166, 172, 178, 179	offval2 6914	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
181	157, 180	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
182	128	resmptd 5452	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
183	128	resmptd 5452	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
184	128	resmptd 5452	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
185	183, 184	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
186	181, 182, 185	3eqtr4d 2666	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
187	113, 186	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
188	112	reseq1d 5395	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $\$
189		xp1st 7198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
190		eldifsni 4320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$
191	189, 190	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
192	191	neneqd 2799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$
193	192	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$
194	193	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$
195	194	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $\$
196		difss 3737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
197		xpss1 5228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
198	196, 197	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
199		resmpt 5449	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$ $\$
200	198, 199	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $\$
201		resmpt 5449	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$ $\$
202	198, 201	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $\$
203	195, 200, 202	3eqtr4rd 2667	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $\$
204	188, 203	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $\$
205		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
206	193, 205	nsyl 135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$
207	206	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$
208	207	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $\$
209		resmpt 5449	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$ $\$
210	198, 209	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $\$
211	208, 210, 202	3eqtr4rd 2667	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $\$
212	188, 211	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $\$
213	135	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
214	111	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
215	213, 214	ifcld 4131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
216		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
217	215, 216	fmptd 6385	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
218		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
219	12, 218	eqeltri 2697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
220	68	anidms 677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
221	159, 220	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
222		elmapg 7870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
223	219, 221, 222	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
224	217, 223	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
225	11, 12	matbas2 20227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
226	159, 114, 225	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
227	226, 13	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
228	224, 227	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
229		simp3 1063	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
230	116	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
231	12, 137	grpsubcl 17495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
232	230, 214, 213, 231	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
233	134	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
234	232, 233	ifcld 4131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
235	234, 214	ifcld 4131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
236		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
237	235, 236	fmptd 6385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
238		elmapg 7870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
239	219, 221, 238	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
240	237, 239	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
241	240, 227	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
242	56	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
243		reseq1 5390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
244	243	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
245		reseq1 5390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
246	245	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$ $\$ $\$
247	245	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$ $\$ $\$
248	244, 246, 247	3anbi123d 1399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$
249		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
250	249	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
251	248, 250	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$
252	251	2ralbidv 2989	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$
253		reseq1 5390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
254	253	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
255	254	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
256		reseq1 5390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
257	256	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$ $\$ $\$
258	255, 257	3anbi12d 1400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$
259		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
260	259	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
261	260	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
262	258, 261	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$
263	262	2ralbidv 2989	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$
264	252, 263	rspc2va 3323	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$
265	229, 241, 242, 264	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
266		reseq1 5390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
267	266	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
268	267	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
269		reseq1 5390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
270	269	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$ $\$ $\$
271	268, 270	3anbi13d 1401	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$
272		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
273	272	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
274	273	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
275	271, 274	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$
276		sneq 4187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
277	276	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
278	277	reseq2d 5396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
279	277	reseq2d 5396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
280	277	reseq2d 5396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
281	279, 280	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
282	278, 281	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
283	276	difeq2d 3728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
284	283	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
285	284	reseq2d 5396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
286	284	reseq2d 5396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
287	285, 286	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$ $\$ $\$
288	284	reseq2d 5396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
289	285, 288	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$ $\$ $\$
290	282, 287, 289	3anbi123d 1399	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$
291	290	imbi1d 331	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$
292	275, 291	rspc2va 3323	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$
293	228, 125, 265, 292	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
294	187, 204, 212, 293	mp3and 1427	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
295	105, 106, 107, 294	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
296		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
297		elequ1 1997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
298	297	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
299	296, 298	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
300	299	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
301	111, 123	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
302	132, 134	ifcld 4131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
303	12, 137	grpsubcl 17495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
304	116, 301, 302, 303	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
305	12, 52, 50	ringridm 18572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
306	114, 304, 305	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
307	306	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
308	300, 307	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
309	142	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
310		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
311	310	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
312	311	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
313	308, 309, 312	3eqtr4d 2666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
314	12, 52, 49	ringrz 18588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
315	114, 304, 314	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
316	315	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
317	316	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
318	151	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
319		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
320	319	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
321	320	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
322	317, 318, 321	3eqtr4d 2666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
323	313, 322	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
324	173	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
325	324, 174	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
326	325	iftrued 4094	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
327	325	iftrued 4094	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
328	327	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
329	323, 326, 328	3eqtr4d 2666	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
330	329	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
331		ovexd 6680	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
332	168, 164	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
333	332, 170	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
334	333	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
335		fconstmpt 5163	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
336	335	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
337	128	resmptd 5452	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
338	161, 331, 334, 336, 337	offval2 6914	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
339	330, 183, 338	3eqtr4d 2666	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
340		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
341		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
342	340, 341	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
343	193, 342	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$
344	343	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $\$
345		resmpt 5449	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$ $\$
346	198, 345	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $\$
347	344, 200, 346	3eqtr4d 2666	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $\$
348	132, 134	ifcld 4131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
349	348	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
350	349, 214	ifcld 4131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
351		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
352	350, 351	fmptd 6385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
353		elmapg 7870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
354	219, 221, 353	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
355	352, 354	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
356	355, 227	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
357	57	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$
358		reseq1 5390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
359	358	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
360		reseq1 5390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$
361	360	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$ $\$ $\$
362	359, 361	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $\$ $\$ $/\$ $\$ $\$
363		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
364	363	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
365	362, 364	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $\$ $\$ $/\$ $\$ $\$
366	365	2ralbidv 2989	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\$ $\$ $/\$ $\$ $\$
367		sneq 4187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
368	367	xpeq2d 5139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
369	368	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
370	369	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
371	370	anbi1d 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $\$ $\$ $/\$ $\$ $\$
372		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
373	372	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
374	371, 373	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $\$ $\$ $/\$ $\$ $\$
375	374	2ralbidv 2989	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\$ $\$ $/\$ $\$ $\$
376	366, 375	rspc2va 3323	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
377	241, 304, 357, 376	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $\$
378		reseq1 5390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
379	378	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
380	379	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
381		reseq1 5390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
382	381	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$ $\$ $\$
383	380, 382	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\$ $\$ $/\$ $\$ $\$
384		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
385	384	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
386	385	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
387	383, 386	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$ $\$ $/\$ $\$ $\$
388	277	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
389	277	reseq2d 5396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
390	388, 389	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
391	279, 390	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
392	284	reseq2d 5396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
393	286, 392	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$ $\$ $\$
394	391, 393	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\$ $\$ $/\$ $\$ $\$
395	394	imbi1d 331	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$ $\$ $/\$ $\$ $\$
396	387, 395	rspc2va 3323	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
397	356, 125, 377, 396	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $\$ $\$
398	339, 347, 397	mp2and 715	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
399	398	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
400	105, 106, 107, 399	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
401		simpl3 1066	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
402		simprlr 803	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
403		simprr 796	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
404		ralss 3668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
405	100, 404	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
406		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
407	406	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$
408		ibar 525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
409	408	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
410		relxp 5227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
411		simpl2 1065	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ $/\$
412	411	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$ $/\$ $/\$
413	412	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$ $/\$ $/\$
414		1st2nd 7214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
415	410, 413, 414	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$
416	415	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ sSet sSet
417		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ $/\$
418		elmapi 7879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
419	418	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ $/\$
420	125	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ $/\$
421		xp2nd 7199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
422	123, 421	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
423	422	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ $/\$
424		fsets 15891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ $/\$ sSet
425	417, 419, 420, 423, 424	syl211anc 1332	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$ $/\$ sSet
426		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 sSet sSet
427	425, 426	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$ sSet
428	427	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
429		xp1st 7198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
430	412, 429	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$ $/\$
431	430	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$
432		fnopfvb 6237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 sSet $/\$ sSet sSet
433	428, 431, 432	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ sSet sSet
434		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 sSet sSet
435	434	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$ $/\$ $/\$ $/\$ sSet sSet
436		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
437		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
438		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
439		fvsetsid 15890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ sSet
440	436, 437, 438, 439	mp3an 1424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 sSet
441	435, 440	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
442	441	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
443		eqcom 2629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
444	442, 443	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
445	416, 433, 444	3bitr2rd 297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
446	123	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$
447		xpopth 7207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
448	413, 446, 447	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
449	409, 445, 448	3bitr3rd 299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
450	449	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
451	407, 450	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
452	451	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
453		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
454	453	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
455	454	con3i 150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
456	455	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
457		elun 3753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $\/$
458	457	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $\/$
459	458	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $\/$
460		orel2 398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $\/$
461	456, 459, 460	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
462	461	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$
463		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
464	463	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$
465		setsres 15901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 sSet $\$ $\$
466	465	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 sSet $\$ $\$
467	436, 466	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ sSet $\$ $\$
468		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
469	468	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
470		df-ne 2795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
471	470	biimpri 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
472		eldifsn 4317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $\$ $/\$
473	469, 471, 472	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $\$
474		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
475	474	opres 5406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $\$ sSet $\$ sSet
476	475	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $\$ sSet $\$ sSet
477		1st2nd2 7205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
478	477	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 sSet sSet
479	478	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $\$ sSet sSet
480	476, 479	bitr4d 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $\$ sSet $\$ sSet
481	412, 473, 480	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ sSet $\$ sSet
482	474	opres 5406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $\$ $\$
483	482	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $\$ $\$
484	477	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
485	484	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $\$
486	483, 485	bitr4d 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $\$ $\$
487	412, 473, 486	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
488	467, 481, 487	3bitr3rd 299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
489	488	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
490	464, 489	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
491		ifeq2 4091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
492	491	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 sSet sSet
493	490, 492	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
494	462, 493	embantd 59	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
495	452, 494	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ sSet
496		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
497	496	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
498		equequ1 1952	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
499	498	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
500		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
501	497, 499, 500	ifbieq12d 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
502	168, 164	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
503		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
504	502, 503	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
505	501, 351, 504	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
506	505	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 sSet sSet
507	412, 506	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ sSet sSet
508	495, 507	sylibrd 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ sSet
509	508	ralimdva 2962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ sSet
510	405, 509	syl5bi 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ sSet
511	510	impr 649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ sSet
512	511	3adantr1 1220	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
513	356	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
514		simpr2 1068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
515	514, 418	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
516	125	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
517	422	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
518	514, 515, 516, 517, 424	syl211anc 1332	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
519	159, 159	elmapd 7871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ sSet sSet
520	519	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ sSet sSet
521	518, 520	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
522		simpr1 1067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
523		raleq 3138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
524	523	imbi1d 331	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
525	524	2ralbidv 2989	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
526	525, 73	elab2g 3353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
527	526	ibi 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
528	522, 527	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
529		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
530	529	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
531	530	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
532		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
533	532	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
534	531, 533	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
535		eleq2 2690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 sSet sSet
536	535	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 sSet sSet
537	536	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 sSet sSet
538	537	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 sSet sSet
539	538	imbi1d 331	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 sSet sSet
540	534, 539	rspc2va 3323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ sSet $/\$ sSet
541	513, 521, 528, 540	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ sSet
542	512, 541	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
543	542	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
544	119	unssad 3790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
545	544	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
546		simpr3 1069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
547		ssel2 3598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
548	547	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
549		elequ1 1997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
550	549	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
551	498, 550, 500	ifbieq12d 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
552	168, 164	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
553	552, 503	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
554	551, 216, 553	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
555	548, 554	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
556		ifeq2 4091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
557	556	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
558		ifid 4125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
559	557, 558	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
560	555, 559	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
561	560	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
562	561	ralimdva 2962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
563	545, 546, 562	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
564	143, 298	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
565	168, 164	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
566	564, 216, 565	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
567	123, 566	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
568	567	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
569		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
570		elequ1 1997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
571	570	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
572	569, 571	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
573	572	ralunsn 4422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
574	121, 573	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
575	563, 568, 574	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
576	228	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
577		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
578	577	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
579	578	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
580		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
581	580	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
582	579, 581	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
583		elequ2 2004	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
584	583	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
585	584	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
586	585	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
587	586	imbi1d 331	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
588	582, 587	rspc2va 3323	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
589	576, 514, 528, 588	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
590	575, 589	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
591	543, 590	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
592	315	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
593	12, 51, 49	grplid 17452	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
594	116, 134, 593	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
595	592, 594	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
596	595	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
597	591, 596	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
598	105, 106, 107, 401, 402, 403, 597	syl33anc 1341	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
599	295, 400, 598	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
600	599	expr 643	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
601	600	ralrimivva 2971	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
602		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . . . 24
603	602	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . 23
604	603	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . 22
605		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23
606	605	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . 22
607	604, 606	imbi12d 334	. . . . . . . . . . . . . . . . . . . . 21
608		elequ2 2004	. . . . . . . . . . . . . . . . . . . . . . . . 25
609	608	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . . . 24
610	609	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . 23
611	610	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . 22
612	611	imbi1d 331	. . . . . . . . . . . . . . . . . . . . 21
613	607, 612	cbvral2v 3179	. . . . . . . . . . . . . . . . . . . 20
614	601, 613	sylib 208	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
615		vex 3203	. . . . . . . . . . . . . . . . . . . 20
616		raleq 3138	. . . . . . . . . . . . . . . . . . . . . 22
617	616	imbi1d 331	. . . . . . . . . . . . . . . . . . . . 21
618	617	2ralbidv 2989	. . . . . . . . . . . . . . . . . . . 20
619	615, 618, 73	elab2 3354	. . . . . . . . . . . . . . . . . . 19
620	614, 619	sylibr 224	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
621	620	3expia 1267	. . . . . . . . . . . . . . . . 17 $/\$
622	621	con3d 148	. . . . . . . . . . . . . . . 16 $/\$
623	622	3adant3 1081	. . . . . . . . . . . . . . 15 $/\$ $/\$
624	623	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
625	624	a2d 29	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
626	104, 625	syl5 34	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
627	83, 88, 93, 98, 99, 626	findcard2s 8201	. . . . . . . . . . 11 $/\$ $/\$
628	78, 627	mpcom 38	. . . . . . . . . 10 $/\$ $/\$
629	628	3exp 1264	. . . . . . . . 9
630	77, 629	mpi 20	. . . . . . . 8
631	76, 630	mt4d 152	. . . . . . 7
632	631	adantr 481	. . . . . 6 $/\$
633		0ex 4790	. . . . . . 7
634		raleq 3138	. . . . . . . . 9
635	634	imbi1d 331	. . . . . . . 8
636	635	2ralbidv 2989	. . . . . . 7
637	633, 636, 73	elab2 3354	. . . . . 6
638	632, 637	sylib 208	. . . . 5 $/\$
639		fveq1 6190	. . . . . . . . 9
640	639	eqeq1d 2624	. . . . . . . 8
641	640	ralbidv 2986	. . . . . . 7
642		fveq2 6191	. . . . . . . 8
643	642	eqeq1d 2624	. . . . . . 7
644	641, 643	imbi12d 334	. . . . . 6
645		eleq2 2690	. . . . . . . . . 10
646	645	ifbid 4108	. . . . . . . . 9
647	646	eqeq2d 2632	. . . . . . . 8
648	647	ralbidv 2986	. . . . . . 7
649	648	imbi1d 331	. . . . . 6
650	644, 649	rspc2va 3323	. . . . 5 $/\$ $/\$
651	2, 9, 638, 650	syl21anc 1325	. . . 4 $/\$
652	1, 651	mpi 20	. . 3 $/\$
653	652	mpteq2dva 4744	. 2
654	54	feqmptd 6249	. 2
655		fconstmpt 5163	. . 3
656	655	a1i 11	. 2
657	653, 654, 656	3eqtr4d 2666	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

cab 2608

wne 2794

wral 2912

cvv 3200 $\$ cdif 3571

cun 3572

wss 3574

c0 3915

cif 4086

csn 4177

cop 4183

cmpt 4729

cid 5023

cxp 5112

cres 5116

wrel 5119

wfn 5883

wf 5884

wf1o 5887

cfv 5888 (class class class)co 6650

cmpt2 6652

cof 6895

c1st 7166

c2nd 7167

cmap 7857

cfn 7955 sSet csts 15855

cbs 15857

cplusg 15941

cmulr 15942

c0g 16100

cgrp 17422

csg 17424

cur 18501

crg 18547 Mat cmat 20213

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-inf2 8538 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 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-xor 1465 df-tru 1486 df-fal 1489 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-se 5074 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-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-tpos 7352 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-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-sup 8348 df-oi 8415 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-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-xnn0 11364 df-z 11378 df-dec 11494 df-uz 11688 df-rp 11833 df-fz 12327 df-fzo 12466 df-seq 12802 df-exp 12861 df-hash 13118 df-word 13299 df-lsw 13300 df-concat 13301 df-s1 13302 df-substr 13303 df-splice 13304 df-reverse 13305 df-s2 13593 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-0g 16102 df-gsum 16103 df-prds 16108 df-pws 16110 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-mhm 17335 df-submnd 17336 df-grp 17425 df-minusg 17426 df-sbg 17427 df-mulg 17541 df-subg 17591 df-ghm 17658 df-gim 17701 df-cntz 17750 df-oppg 17776 df-symg 17798 df-pmtr 17862 df-psgn 17911 df-evpm 17912 df-cmn 18195 df-abl 18196 df-mgp 18490 df-ur 18502 df-ring 18549 df-cring 18550 df-oppr 18623 df-dvdsr 18641 df-unit 18642 df-invr 18672 df-dvr 18683 df-rnghom 18715 df-drng 18749 df-subrg 18778 df-lmod 18865 df-lss 18933 df-sra 19172 df-rgmod 19173 df-cnfld 19747 df-zring 19819 df-zrh 19852 df-dsmm 20076 df-frlm 20091 df-mamu 20190 df-mat 20214

This theorem is referenced by: mdetuni0 20427

W3C validator