seqf1oglem1 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > seqf1oglem1		Unicode version

Theorem seqf1oglem1 10613

Description: Lemma for seqf1og 10615. (Contributed by Mario Carneiro, 26-Feb-2014.) (Revised by Mario Carneiro, 27-May-2014.)

**Hypotheses**
Ref	Expression
seqf1o.1	$/\$ $/\$
seqf1o.2	$/\$ $/\$
seqf1o.3	$/\$ $/\$ $/\$
seqf1o.4
seqf1o.5
seqf1og.p
seqf1olem.5
seqf1olem.6
seqf1olem.7
seqf1olem.8

**Assertion**
Ref	Expression
seqf1oglem1

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

**Proof of Theorem seqf1oglem1**
Step	Hyp	Ref	Expression
1		seqf1olem.7	. 2
2		seqf1olem.5	. . . . 5
3		f1of 5505	. . . . 5
4	2, 3	syl 14	. . . 4
5	4	adantr 276	. . 3 $/\$
6		fzelp1 10151	. . . . 5
7	6	adantl 277	. . . 4 $/\$
8		fzp1elp1 10152	. . . . 5
9	8	adantl 277	. . . 4 $/\$
10		elfzelz 10102	. . . . 5
11		seqf1olem.8	. . . . . . 7
12		f1ocnv 5518	. . . . . . . . . . 11
13	2, 12	syl 14	. . . . . . . . . 10
14		f1of1 5504	. . . . . . . . . 10
15	13, 14	syl 14	. . . . . . . . 9
16		f1f 5464	. . . . . . . . 9
17	15, 16	syl 14	. . . . . . . 8
18		seqf1o.4	. . . . . . . . . 10
19		peano2uz 9659	. . . . . . . . . 10
20	18, 19	syl 14	. . . . . . . . 9
21		eluzfz2 10109	. . . . . . . . 9
22	20, 21	syl 14	. . . . . . . 8
23	17, 22	ffvelcdmd 5699	. . . . . . 7
24	11, 23	eqeltrid 2283	. . . . . 6
25	24	elfzelzd 10103	. . . . 5
26		zdclt 9405	. . . . 5 $/\$ DECID
27	10, 25, 26	syl2anr 290	. . . 4 $/\$ DECID
28	7, 9, 27	ifcldcd 3598	. . 3 $/\$
29	5, 28	ffvelcdmd 5699	. 2 $/\$
30	17	adantr 276	. . . . 5 $/\$
31		fzelp1 10151	. . . . . 6
32	31	adantl 277	. . . . 5 $/\$
33	30, 32	ffvelcdmd 5699	. . . 4 $/\$
34	33	elfzelzd 10103	. . 3 $/\$
35		peano2zm 9366	. . . 4
36	34, 35	syl 14	. . 3 $/\$
37	25	adantr 276	. . . 4 $/\$
38		zdclt 9405	. . . 4 $/\$ DECID
39	34, 37, 38	syl2anc 411	. . 3 $/\$ DECID
40	34, 36, 39	ifcldcd 3598	. 2 $/\$
41		iftrue 3567	. . . . . . . . 9
42	41	fveq2d 5563	. . . . . . . 8
43	42	eqeq2d 2208	. . . . . . 7
44	43	adantl 277	. . . . . 6 $/\$ $/\$
45		simprr 531	. . . . . . . . 9 $/\$ $/\$ $/\$
46	5, 7	ffvelcdmd 5699	. . . . . . . . . . . . 13 $/\$
47	46	elfzelzd 10103	. . . . . . . . . . . 12 $/\$
48		eluzel2 9608	. . . . . . . . . . . . . 14
49	18, 48	syl 14	. . . . . . . . . . . . 13
50	49	adantr 276	. . . . . . . . . . . 12 $/\$
51		uzssz 9623	. . . . . . . . . . . . . 14
52	51, 18	sselid 3182	. . . . . . . . . . . . 13
53	52	adantr 276	. . . . . . . . . . . 12 $/\$
54		fzdcel 10117	. . . . . . . . . . . 12 $/\$ $/\$ DECID
55	47, 50, 53, 54	syl3anc 1249	. . . . . . . . . . 11 $/\$ DECID
56	55	adantr 276	. . . . . . . . . 10 $/\$ $/\$ $/\$ DECID
57	10	zred 9450	. . . . . . . . . . . 12
58	57	ad2antlr 489	. . . . . . . . . . 11 $/\$ $/\$ $/\$
59		simprl 529	. . . . . . . . . . 11 $/\$ $/\$ $/\$
60	58, 59	gtned 8141	. . . . . . . . . 10 $/\$ $/\$ $/\$
61	4	ad2antrr 488	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
62		fzssp1 10144	. . . . . . . . . . . . . . . . 17
63		simplr 528	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
64	62, 63	sselid 3182	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
65	61, 64	ffvelcdmd 5699	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
66		elfzp1 10149	. . . . . . . . . . . . . . . . 17 $\/$
67	18, 66	syl 14	. . . . . . . . . . . . . . . 16 $\/$
68	67	ad2antrr 488	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\/$
69	65, 68	mpbid 147	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\/$
70	69	ord 725	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
71	2	ad2antrr 488	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
72		f1ocnvfv 5827	. . . . . . . . . . . . . . 15 $/\$
73	71, 64, 72	syl2anc 411	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
74	11	eqeq1i 2204	. . . . . . . . . . . . . 14
75	73, 74	imbitrrdi 162	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
76	70, 75	syld 45	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
77	76	a1d 22	. . . . . . . . . . 11 $/\$ $/\$ $/\$ DECID
78	77	necon1addc 2443	. . . . . . . . . 10 $/\$ $/\$ $/\$ DECID
79	56, 60, 78	mp2d 47	. . . . . . . . 9 $/\$ $/\$ $/\$
80	45, 79	eqeltrd 2273	. . . . . . . 8 $/\$ $/\$ $/\$
81	45	eqcomd 2202	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
82		f1ocnvfv 5827	. . . . . . . . . . . . 13 $/\$
83	71, 64, 82	syl2anc 411	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
84	81, 83	mpd 13	. . . . . . . . . . 11 $/\$ $/\$ $/\$
85	84, 59	eqbrtrd 4056	. . . . . . . . . 10 $/\$ $/\$ $/\$
86		iftrue 3567	. . . . . . . . . 10
87	85, 86	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$
88	87, 84	eqtr2d 2230	. . . . . . . 8 $/\$ $/\$ $/\$
89	80, 88	jca 306	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
90	89	expr 375	. . . . . 6 $/\$ $/\$ $/\$
91	44, 90	sylbid 150	. . . . 5 $/\$ $/\$ $/\$
92		iffalse 3570	. . . . . . . . 9
93	92	fveq2d 5563	. . . . . . . 8
94	93	eqeq2d 2208	. . . . . . 7
95	94	adantl 277	. . . . . 6 $/\$ $/\$
96		simprr 531	. . . . . . . . 9 $/\$ $/\$ $/\$
97	5, 9	ffvelcdmd 5699	. . . . . . . . . . . . 13 $/\$
98	97	elfzelzd 10103	. . . . . . . . . . . 12 $/\$
99		fzdcel 10117	. . . . . . . . . . . 12 $/\$ $/\$ DECID
100	98, 50, 53, 99	syl3anc 1249	. . . . . . . . . . 11 $/\$ DECID
101	100	adantr 276	. . . . . . . . . 10 $/\$ $/\$ $/\$ DECID
102	25	zred 9450	. . . . . . . . . . . 12
103	102	ad2antrr 488	. . . . . . . . . . 11 $/\$ $/\$ $/\$
104	57	ad2antlr 489	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
105		peano2re 8164	. . . . . . . . . . . . 13
106	104, 105	syl 14	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
107		simprl 529	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
108	103, 104, 107	nltled 8149	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
109	104	ltp1d 8959	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
110	103, 104, 106, 108, 109	lelttrd 8153	. . . . . . . . . . 11 $/\$ $/\$ $/\$
111	103, 110	ltned 8142	. . . . . . . . . 10 $/\$ $/\$ $/\$
112	4	ad2antrr 488	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
113	8	ad2antlr 489	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
114	112, 113	ffvelcdmd 5699	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
115		elfzp1 10149	. . . . . . . . . . . . . . . . 17 $\/$
116	18, 115	syl 14	. . . . . . . . . . . . . . . 16 $\/$
117	116	ad2antrr 488	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\/$
118	114, 117	mpbid 147	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\/$
119	118	ord 725	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
120	2	ad2antrr 488	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
121		f1ocnvfv 5827	. . . . . . . . . . . . . . 15 $/\$
122	120, 113, 121	syl2anc 411	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
123	11	eqeq1i 2204	. . . . . . . . . . . . . 14
124	122, 123	imbitrrdi 162	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
125	119, 124	syld 45	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
126	125	a1d 22	. . . . . . . . . . 11 $/\$ $/\$ $/\$ DECID
127	126	necon1addc 2443	. . . . . . . . . 10 $/\$ $/\$ $/\$ DECID
128	101, 111, 127	mp2d 47	. . . . . . . . 9 $/\$ $/\$ $/\$
129	96, 128	eqeltrd 2273	. . . . . . . 8 $/\$ $/\$ $/\$
130	96	eqcomd 2202	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
131		f1ocnvfv 5827	. . . . . . . . . . . . . . 15 $/\$
132	120, 113, 131	syl2anc 411	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
133	130, 132	mpd 13	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
134	133	breq1d 4044	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
135		lttr 8102	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
136	104, 106, 103, 135	syl3anc 1249	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
137	109, 136	mpand 429	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
138	134, 137	sylbid 150	. . . . . . . . . . 11 $/\$ $/\$ $/\$
139	107, 138	mtod 664	. . . . . . . . . 10 $/\$ $/\$ $/\$
140		iffalse 3570	. . . . . . . . . 10
141	139, 140	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$
142	133	oveq1d 5938	. . . . . . . . 9 $/\$ $/\$ $/\$
143	104	recnd 8057	. . . . . . . . . 10 $/\$ $/\$ $/\$
144		ax-1cn 7974	. . . . . . . . . 10
145		pncan 8234	. . . . . . . . . 10 $/\$
146	143, 144, 145	sylancl 413	. . . . . . . . 9 $/\$ $/\$ $/\$
147	141, 142, 146	3eqtrrd 2234	. . . . . . . 8 $/\$ $/\$ $/\$
148	129, 147	jca 306	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
149	148	expr 375	. . . . . 6 $/\$ $/\$ $/\$
150	95, 149	sylbid 150	. . . . 5 $/\$ $/\$ $/\$
151		exmiddc 837	. . . . . 6 DECID $\/$
152	27, 151	syl 14	. . . . 5 $/\$ $\/$
153	91, 150, 152	mpjaodan 799	. . . 4 $/\$ $/\$
154	153	expimpd 363	. . 3 $/\$ $/\$
155	86	eqeq2d 2208	. . . . . . 7
156	155	adantl 277	. . . . . 6 $/\$ $/\$
157	49	ad2antrr 488	. . . . . . . . 9 $/\$ $/\$ $/\$
158		eluzelz 9612	. . . . . . . . . . 11
159	18, 158	syl 14	. . . . . . . . . 10
160	159	ad2antrr 488	. . . . . . . . 9 $/\$ $/\$ $/\$
161		simprr 531	. . . . . . . . . . 11 $/\$ $/\$ $/\$
162	17	ad2antrr 488	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
163		simplr 528	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
164	62, 163	sselid 3182	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
165	162, 164	ffvelcdmd 5699	. . . . . . . . . . 11 $/\$ $/\$ $/\$
166	161, 165	eqeltrd 2273	. . . . . . . . . 10 $/\$ $/\$ $/\$
167	166	elfzelzd 10103	. . . . . . . . 9 $/\$ $/\$ $/\$
168		elfzle1 10104	. . . . . . . . . 10
169	166, 168	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$
170	167	zred 9450	. . . . . . . . . . 11 $/\$ $/\$ $/\$
171	102	ad2antrr 488	. . . . . . . . . . 11 $/\$ $/\$ $/\$
172	159	peano2zd 9453	. . . . . . . . . . . . 13
173	172	zred 9450	. . . . . . . . . . . 12
174	173	ad2antrr 488	. . . . . . . . . . 11 $/\$ $/\$ $/\$
175		simprl 529	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
176	161, 175	eqbrtrd 4056	. . . . . . . . . . 11 $/\$ $/\$ $/\$
177		elfzle2 10105	. . . . . . . . . . . . 13
178	24, 177	syl 14	. . . . . . . . . . . 12
179	178	ad2antrr 488	. . . . . . . . . . 11 $/\$ $/\$ $/\$
180	170, 171, 174, 176, 179	ltletrd 8452	. . . . . . . . . 10 $/\$ $/\$ $/\$
181		zleltp1 9383	. . . . . . . . . . 11 $/\$
182	167, 160, 181	syl2anc 411	. . . . . . . . . 10 $/\$ $/\$ $/\$
183	180, 182	mpbird 167	. . . . . . . . 9 $/\$ $/\$ $/\$
184	157, 160, 167, 169, 183	elfzd 10093	. . . . . . . 8 $/\$ $/\$ $/\$
185	176, 42	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$
186	161	fveq2d 5563	. . . . . . . . 9 $/\$ $/\$ $/\$
187	2	ad2antrr 488	. . . . . . . . . 10 $/\$ $/\$ $/\$
188		f1ocnvfv2 5826	. . . . . . . . . 10 $/\$
189	187, 164, 188	syl2anc 411	. . . . . . . . 9 $/\$ $/\$ $/\$
190	185, 186, 189	3eqtrrd 2234	. . . . . . . 8 $/\$ $/\$ $/\$
191	184, 190	jca 306	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
192	191	expr 375	. . . . . 6 $/\$ $/\$ $/\$
193	156, 192	sylbid 150	. . . . 5 $/\$ $/\$ $/\$
194	140	eqeq2d 2208	. . . . . . 7
195	194	adantl 277	. . . . . 6 $/\$ $/\$
196	49	ad2antrr 488	. . . . . . . . 9 $/\$ $/\$ $/\$
197	159	ad2antrr 488	. . . . . . . . 9 $/\$ $/\$ $/\$
198		simprr 531	. . . . . . . . . 10 $/\$ $/\$ $/\$
199	17	ad2antrr 488	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
200		simplr 528	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
201	62, 200	sselid 3182	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
202	199, 201	ffvelcdmd 5699	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
203	202	elfzelzd 10103	. . . . . . . . . . 11 $/\$ $/\$ $/\$
204	203, 35	syl 14	. . . . . . . . . 10 $/\$ $/\$ $/\$
205	198, 204	eqeltrd 2273	. . . . . . . . 9 $/\$ $/\$ $/\$
206	49	zred 9450	. . . . . . . . . . 11
207	206	ad2antrr 488	. . . . . . . . . 10 $/\$ $/\$ $/\$
208	102	ad2antrr 488	. . . . . . . . . 10 $/\$ $/\$ $/\$
209	205	zred 9450	. . . . . . . . . 10 $/\$ $/\$ $/\$
210		elfzle1 10104	. . . . . . . . . . . 12
211	24, 210	syl 14	. . . . . . . . . . 11
212	211	ad2antrr 488	. . . . . . . . . 10 $/\$ $/\$ $/\$
213		elfzelz 10102	. . . . . . . . . . . . . . . . . . . . 21
214	213	adantl 277	. . . . . . . . . . . . . . . . . . . 20 $/\$
215	214	zred 9450	. . . . . . . . . . . . . . . . . . 19 $/\$
216	159	zred 9450	. . . . . . . . . . . . . . . . . . . . 21
217	216	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$
218	173	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$
219		elfzle2 10105	. . . . . . . . . . . . . . . . . . . . 21
220	219	adantl 277	. . . . . . . . . . . . . . . . . . . 20 $/\$
221	217	ltp1d 8959	. . . . . . . . . . . . . . . . . . . 20 $/\$
222	215, 217, 218, 220, 221	lelttrd 8153	. . . . . . . . . . . . . . . . . . 19 $/\$
223	215, 222	gtned 8141	. . . . . . . . . . . . . . . . . 18 $/\$
224	223	adantr 276	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
225	15	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
226	22	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
227		f1fveq 5820	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
228	225, 226, 201, 227	syl12anc 1247	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
229	228	necon3bid 2408	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
230	224, 229	mpbird 167	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
231	11	neeq1i 2382	. . . . . . . . . . . . . . . 16
232	230, 231	sylibr 134	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
233	232	necomd 2453	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
234	25	ad2antrr 488	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
235		zapne 9402	. . . . . . . . . . . . . . 15 $/\$ #
236	203, 234, 235	syl2anc 411	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ #
237	233, 236	mpbird 167	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ #
238	203	zred 9450	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
239		simprl 529	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
240	208, 238, 239	nltled 8149	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
241	208, 238, 240	leltapd 8668	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ #
242	237, 241	mpbird 167	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
243		zltlem1 9385	. . . . . . . . . . . . 13 $/\$
244	234, 203, 243	syl2anc 411	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
245	242, 244	mpbid 147	. . . . . . . . . . 11 $/\$ $/\$ $/\$
246	245, 198	breqtrrd 4062	. . . . . . . . . 10 $/\$ $/\$ $/\$
247	207, 208, 209, 212, 246	letrd 8152	. . . . . . . . 9 $/\$ $/\$ $/\$
248		elfzle2 10105	. . . . . . . . . . . 12
249	202, 248	syl 14	. . . . . . . . . . 11 $/\$ $/\$ $/\$
250	216	ad2antrr 488	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
251		1re 8027	. . . . . . . . . . . . 13
252		lesubadd 8463	. . . . . . . . . . . . 13 $/\$ $/\$
253	251, 252	mp3an2 1336	. . . . . . . . . . . 12 $/\$
254	238, 250, 253	syl2anc 411	. . . . . . . . . . 11 $/\$ $/\$ $/\$
255	249, 254	mpbird 167	. . . . . . . . . 10 $/\$ $/\$ $/\$
256	198, 255	eqbrtrd 4056	. . . . . . . . 9 $/\$ $/\$ $/\$
257	196, 197, 205, 247, 256	elfzd 10093	. . . . . . . 8 $/\$ $/\$ $/\$
258	208, 209, 246	lensymd 8150	. . . . . . . . . 10 $/\$ $/\$ $/\$
259	258, 93	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$
260	198	oveq1d 5938	. . . . . . . . . . 11 $/\$ $/\$ $/\$
261	203	zcnd 9451	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
262		npcan 8237	. . . . . . . . . . . 12 $/\$
263	261, 144, 262	sylancl 413	. . . . . . . . . . 11 $/\$ $/\$ $/\$
264	260, 263	eqtrd 2229	. . . . . . . . . 10 $/\$ $/\$ $/\$
265	264	fveq2d 5563	. . . . . . . . 9 $/\$ $/\$ $/\$
266	2	ad2antrr 488	. . . . . . . . . 10 $/\$ $/\$ $/\$
267	266, 201, 188	syl2anc 411	. . . . . . . . 9 $/\$ $/\$ $/\$
268	259, 265, 267	3eqtrrd 2234	. . . . . . . 8 $/\$ $/\$ $/\$
269	257, 268	jca 306	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
270	269	expr 375	. . . . . 6 $/\$ $/\$ $/\$
271	195, 270	sylbid 150	. . . . 5 $/\$ $/\$ $/\$
272		exmiddc 837	. . . . . 6 DECID $\/$
273	39, 272	syl 14	. . . . 5 $/\$ $\/$
274	193, 271, 273	mpjaodan 799	. . . 4 $/\$ $/\$
275	274	expimpd 363	. . 3 $/\$ $/\$
276	154, 275	impbid 129	. 2 $/\$ $/\$
277	1, 29, 40, 276	f1od 6127	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 709 DECID wdc 835 $/\$ w3a 980

wceq 1364

wcel 2167

wne 2367

wss 3157

cif 3562 class class class wbr 4034

cmpt 4095

ccnv 4663

wf 5255

wf1 5256

wf1o 5258

cfv 5259 (class class class)co 5923

cc 7879

cr 7880

c1 7882

caddc 7884

clt 8063

cle 8064

cmin 8199 # cap 8610

cz 9328

cuz 9603

cfz 10085

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-sep 4152 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-cnex 7972 ax-resscn 7973 ax-1cn 7974 ax-1re 7975 ax-icn 7976 ax-addcl 7977 ax-addrcl 7978 ax-mulcl 7979 ax-mulrcl 7980 ax-addcom 7981 ax-mulcom 7982 ax-addass 7983 ax-mulass 7984 ax-distr 7985 ax-i2m1 7986 ax-0lt1 7987 ax-1rid 7988 ax-0id 7989 ax-rnegex 7990 ax-precex 7991 ax-cnre 7992 ax-pre-ltirr 7993 ax-pre-ltwlin 7994 ax-pre-lttrn 7995 ax-pre-apti 7996 ax-pre-ltadd 7997 ax-pre-mulgt0 7998

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rab 2484 df-v 2765 df-sbc 2990 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-if 3563 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-br 4035 df-opab 4096 df-mpt 4097 df-id 4329 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-riota 5878 df-ov 5926 df-oprab 5927 df-mpo 5928 df-pnf 8065 df-mnf 8066 df-xr 8067 df-ltxr 8068 df-le 8069 df-sub 8201 df-neg 8202 df-reap 8604 df-ap 8611 df-inn 8993 df-n0 9252 df-z 9329 df-uz 9604 df-fz 10086

This theorem is referenced by: seqf1oglem2 10614

W3C validator