axdc4lem - Metamath Proof Explorer

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

Theorem axdc4lem 9277

Description: Lemma for axdc4 9278. (Contributed by Mario Carneiro, 31-Jan-2013.) (Revised by Mario Carneiro, 16-Nov-2013.)

**Hypotheses**
Ref	Expression
axdc4lem.1
axdc4lem.2

**Assertion**
Ref	Expression
axdc4lem	$/\$ $\$ $/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

Proof of Theorem axdc4lem Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		peano1 7085	. . . 4
2		opelxpi 5148	. . . 4 $/\$
3	1, 2	mpan 706	. . 3
4		simp2 1062	. . . . . . . 8 $\$ $/\$ $/\$
5		fovrn 6804	. . . . . . . 8 $\$ $/\$ $/\$ $\$
6		peano2 7086	. . . . . . . . . . 11
7	6	snssd 4340	. . . . . . . . . 10
8		eldifi 3732	. . . . . . . . . 10 $\$
9		axdc4lem.1	. . . . . . . . . . . 12
10	9	elpw2 4828	. . . . . . . . . . 11
11		xpss12 5225	. . . . . . . . . . 11 $/\$
12	10, 11	sylan2b 492	. . . . . . . . . 10 $/\$
13	7, 8, 12	syl2an 494	. . . . . . . . 9 $/\$ $\$
14		snex 4908	. . . . . . . . . . 11
15		ovex 6678	. . . . . . . . . . 11
16	14, 15	xpex 6962	. . . . . . . . . 10
17	16	elpw 4164	. . . . . . . . 9
18	13, 17	sylibr 224	. . . . . . . 8 $/\$ $\$
19	4, 5, 18	syl2anc 693	. . . . . . 7 $\$ $/\$ $/\$
20		eldifn 3733	. . . . . . . 8 $\$
21	15	elsn 4192	. . . . . . . . . . 11
22	21	necon3bbii 2841	. . . . . . . . . 10
23		vex 3203	. . . . . . . . . . . . 13
24	23	sucex 7011	. . . . . . . . . . . 12
25	24	snnz 4309	. . . . . . . . . . 11
26		xpnz 5553	. . . . . . . . . . . 12 $/\$
27	26	biimpi 206	. . . . . . . . . . 11 $/\$
28	25, 27	mpan 706	. . . . . . . . . 10
29	22, 28	sylbi 207	. . . . . . . . 9
30	16	elsn 4192	. . . . . . . . . 10
31	30	necon3bbii 2841	. . . . . . . . 9
32	29, 31	sylibr 224	. . . . . . . 8
33	5, 20, 32	3syl 18	. . . . . . 7 $\$ $/\$ $/\$
34	19, 33	eldifd 3585	. . . . . 6 $\$ $/\$ $/\$ $\$
35	34	3expib 1268	. . . . 5 $\$ $/\$ $\$
36	35	ralrimivv 2970	. . . 4 $\$ $\$
37		axdc4lem.2	. . . . 5
38	37	fmpt2 7237	. . . 4 $\$ $\$
39	36, 38	sylib 208	. . 3 $\$ $\$
40		dcomex 9269	. . . . 5
41	40, 9	xpex 6962	. . . 4
42	41	axdc3 9276	. . 3 $/\$ $\$ $/\$ $/\$
43	3, 39, 42	syl2an 494	. 2 $/\$ $\$ $/\$ $/\$
44		2ndcof 7197	. . . . . . . . 9
45	44	3ad2ant1 1082	. . . . . . . 8 $/\$ $/\$
46	45	adantl 482	. . . . . . 7 $/\$ $/\$ $/\$
47		fex2 7121	. . . . . . . 8 $/\$ $/\$
48	40, 9, 47	mp3an23 1416	. . . . . . 7
49	46, 48	syl 17	. . . . . 6 $/\$ $/\$ $/\$
50		fvco3 6275	. . . . . . . . . . 11 $/\$
51	1, 50	mpan2 707	. . . . . . . . . 10
52	51	3ad2ant1 1082	. . . . . . . . 9 $/\$ $/\$
53		fveq2 6191	. . . . . . . . . 10
54	53	3ad2ant2 1083	. . . . . . . . 9 $/\$ $/\$
55	52, 54	eqtrd 2656	. . . . . . . 8 $/\$ $/\$
56		op2ndg 7181	. . . . . . . . 9 $/\$
57	1, 56	mpan 706	. . . . . . . 8
58	55, 57	sylan9eqr 2678	. . . . . . 7 $/\$ $/\$ $/\$
59		nfv 1843	. . . . . . . . 9
60		nfv 1843	. . . . . . . . . 10
61		nfv 1843	. . . . . . . . . 10
62		nfra1 2941	. . . . . . . . . 10
63	60, 61, 62	nf3an 1831	. . . . . . . . 9 $/\$ $/\$
64	59, 63	nfan 1828	. . . . . . . 8 $/\$ $/\$ $/\$
65		fveq2 6191	. . . . . . . . . . . . . . . . 17
66		opeq1 4402	. . . . . . . . . . . . . . . . 17
67	65, 66	eqeq12d 2637	. . . . . . . . . . . . . . . 16
68	67	exbidv 1850	. . . . . . . . . . . . . . 15
69		fveq2 6191	. . . . . . . . . . . . . . . . 17
70		opeq1 4402	. . . . . . . . . . . . . . . . 17
71	69, 70	eqeq12d 2637	. . . . . . . . . . . . . . . 16
72	71	exbidv 1850	. . . . . . . . . . . . . . 15
73		fveq2 6191	. . . . . . . . . . . . . . . . 17
74		opeq1 4402	. . . . . . . . . . . . . . . . 17
75	73, 74	eqeq12d 2637	. . . . . . . . . . . . . . . 16
76	75	exbidv 1850	. . . . . . . . . . . . . . 15
77		opeq2 4403	. . . . . . . . . . . . . . . . . . 19
78	77	eqeq2d 2632	. . . . . . . . . . . . . . . . . 18
79	78	spcegv 3294	. . . . . . . . . . . . . . . . 17
80	79	imp 445	. . . . . . . . . . . . . . . 16 $/\$
81	80	3ad2antr2 1227	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
82		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
83		df-ov 6653	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
84	82, 83	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . . . . . . 26
85	84	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
86		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
87		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
88		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
89		opelxp2 5151	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
90	88, 89	syl6bi 243	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
91	87, 90	mpan9 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
92		suceq 5790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
93	92	sneqd 4189	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
94		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
95	93, 94	xpeq12d 5140	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
96		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
97	96	xpeq2d 5139	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
98		snex 4908	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
99		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
100	98, 99	xpex 6962	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
101	95, 97, 37, 100	ovmpt2 6796	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
102	86, 91, 101	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
103	85, 102	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
104		suceq 5790	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
105	104	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
106		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
107	106	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
108	105, 107	eleq12d 2695	. . . . . . . . . . . . . . . . . . . . . . . . . 26
109	108	rspcv 3305	. . . . . . . . . . . . . . . . . . . . . . . . 25
110	109	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
111		eleq2 2690	. . . . . . . . . . . . . . . . . . . . . . . . 25
112		elxp 5131	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
113		velsn 4193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
114		opeq1 4402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
115	113, 114	sylbi 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
116	115	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
117	116	biimpac 503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
118	117	adantrr 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
119	118	eximi 1762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
120	119	exlimiv 1858	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
121	112, 120	sylbi 207	. . . . . . . . . . . . . . . . . . . . . . . . 25
122	111, 121	syl6bi 243	. . . . . . . . . . . . . . . . . . . . . . . 24
123	103, 110, 122	sylsyld 61	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
124	123	expcom 451	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
125	124	exlimiv 1858	. . . . . . . . . . . . . . . . . . . . 21 $/\$
126	125	com3l 89	. . . . . . . . . . . . . . . . . . . 20 $/\$
127		opeq2 4403	. . . . . . . . . . . . . . . . . . . . . 22
128	127	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . 21
129	128	cbvexv 2275	. . . . . . . . . . . . . . . . . . . 20
130	126, 129	syl8ib 246	. . . . . . . . . . . . . . . . . . 19 $/\$
131	130	impancom 456	. . . . . . . . . . . . . . . . . 18 $/\$
132	131	3adant2 1080	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
133	132	adantl 482	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
134	133	com12 32	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
135	68, 72, 76, 81, 134	finds2 7094	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
136	135	com12 32	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
137	136	ralrimiv 2965	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
138		fveq2 6191	. . . . . . . . . . . . . . 15
139		opeq1 4402	. . . . . . . . . . . . . . 15
140	138, 139	eqeq12d 2637	. . . . . . . . . . . . . 14
141	140	exbidv 1850	. . . . . . . . . . . . 13
142	141	rspccv 3306	. . . . . . . . . . . 12
143	137, 142	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$
144	143	3impia 1261	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
145		simp21 1094	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
146		simp3 1063	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
147		rspa 2930	. . . . . . . . . . . 12 $/\$
148	147	3ad2antl3 1225	. . . . . . . . . . 11 $/\$ $/\$ $/\$
149	148	3adant1 1079	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
150		simpl 473	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
151	150	fveq2d 6195	. . . . . . . . . . . . . . . 16 $/\$ $/\$
152		simprr 796	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
153		ffvelrn 6357	. . . . . . . . . . . . . . . . . . 19 $/\$
154		eleq1 2689	. . . . . . . . . . . . . . . . . . . 20
155		opelxp2 5151	. . . . . . . . . . . . . . . . . . . 20
156	154, 155	syl6bi 243	. . . . . . . . . . . . . . . . . . 19
157	153, 156	syl5 34	. . . . . . . . . . . . . . . . . 18 $/\$
158	157	imp 445	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
159		df-ov 6653	. . . . . . . . . . . . . . . . . 18
160		suceq 5790	. . . . . . . . . . . . . . . . . . . . 21
161	160	sneqd 4189	. . . . . . . . . . . . . . . . . . . 20
162		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20
163	161, 162	xpeq12d 5140	. . . . . . . . . . . . . . . . . . 19
164		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20
165	164	xpeq2d 5139	. . . . . . . . . . . . . . . . . . 19
166		snex 4908	. . . . . . . . . . . . . . . . . . . 20
167		ovex 6678	. . . . . . . . . . . . . . . . . . . 20
168	166, 167	xpex 6962	. . . . . . . . . . . . . . . . . . 19
169	163, 165, 37, 168	ovmpt2 6796	. . . . . . . . . . . . . . . . . 18 $/\$
170	159, 169	syl5eqr 2670	. . . . . . . . . . . . . . . . 17 $/\$
171	152, 158, 170	syl2anc 693	. . . . . . . . . . . . . . . 16 $/\$ $/\$
172	151, 171	eqtrd 2656	. . . . . . . . . . . . . . 15 $/\$ $/\$
173	172	eleq2d 2687	. . . . . . . . . . . . . 14 $/\$ $/\$
174		elxp 5131	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
175		peano2 7086	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
176		fvco3 6275	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
177	175, 176	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
178	177	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
179		simpll 790	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
180	179	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
181	178, 180	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
182		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . 25
183		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . 25
184	182, 183	op2nd 7177	. . . . . . . . . . . . . . . . . . . . . . . 24
185	181, 184	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
186		fvco3 6275	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
187	186	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
188		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
189	188	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
190	187, 189	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
191		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . 26
192		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . 26
193	191, 192	op2nd 7177	. . . . . . . . . . . . . . . . . . . . . . . . 25
194	190, 193	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
195	194	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
196	185, 195	eleq12d 2695	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
197	196	biimprcd 240	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
198	197	exp4c 636	. . . . . . . . . . . . . . . . . . . 20 $/\$
199	198	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
200	199	impcom 446	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
201	200	exlimivv 1860	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
202	174, 201	sylbi 207	. . . . . . . . . . . . . . . 16 $/\$
203	202	com3l 89	. . . . . . . . . . . . . . 15 $/\$
204	203	imp 445	. . . . . . . . . . . . . 14 $/\$ $/\$
205	173, 204	sylbid 230	. . . . . . . . . . . . 13 $/\$ $/\$
206	205	ex 450	. . . . . . . . . . . 12 $/\$
207	206	exlimiv 1858	. . . . . . . . . . 11 $/\$
208	207	3imp 1256	. . . . . . . . . 10 $/\$ $/\$ $/\$
209	144, 145, 146, 149, 208	syl121anc 1331	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
210	209	3expia 1267	. . . . . . . 8 $/\$ $/\$ $/\$
211	64, 210	ralrimi 2957	. . . . . . 7 $/\$ $/\$ $/\$
212	46, 58, 211	3jca 1242	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
213		feq1 6026	. . . . . . . 8
214		fveq1 6190	. . . . . . . . 9
215	214	eqeq1d 2624	. . . . . . . 8
216		fveq1 6190	. . . . . . . . . 10
217		fveq1 6190	. . . . . . . . . . 11
218	217	oveq2d 6666	. . . . . . . . . 10
219	216, 218	eleq12d 2695	. . . . . . . . 9
220	219	ralbidv 2986	. . . . . . . 8
221	213, 215, 220	3anbi123d 1399	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
222	221	spcegv 3294	. . . . . 6 $/\$ $/\$ $/\$ $/\$
223	49, 212, 222	sylc 65	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
224	223	ex 450	. . . 4 $/\$ $/\$ $/\$ $/\$
225	224	exlimdv 1861	. . 3 $/\$ $/\$ $/\$ $/\$
226	225	adantr 481	. 2 $/\$ $\$ $/\$ $/\$ $/\$ $/\$
227	43, 226	mpd 15	1 $/\$ $\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wex 1704

wcel 1990

wne 2794

wral 2912

cvv 3200 $\$ cdif 3571

wss 3574

c0 3915

cpw 4158

csn 4177

cop 4183

cxp 5112

ccom 5118

csuc 5725

wf 5884

cfv 5888 (class class class)co 6650

cmpt2 6652

com 7065

c2nd 7167

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-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-dc 9268

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-ral 2917 df-rex 2918 df-reu 2919 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-uni 4437 df-iun 4522 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-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-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-1o 7560

This theorem is referenced by: axdc4 9278

W3C validator