infxpenlem - Metamath Proof Explorer

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

Theorem infxpenlem 8836

Description: Lemma for infxpen 8837. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.)

**Hypotheses**
Ref	Expression
leweon.1	$/\$ $/\$ $\/$ $/\$
r0weon.1	$/\$ $/\$ $\/$ $/\$
infxpen.1
infxpen.2	$/\$ $/\$ $/\$
infxpen.3
infxpen.4	OrdIso

**Assertion**
Ref	Expression
infxpenlem	$/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

**Proof of Theorem infxpenlem**
Step	Hyp	Ref	Expression
1		sseq2 3627	. . . 4
2		xpeq12 5134	. . . . . 6 $/\$
3	2	anidms 677	. . . . 5
4		id 22	. . . . 5
5	3, 4	breq12d 4666	. . . 4
6	1, 5	imbi12d 334	. . 3
7		sseq2 3627	. . . 4
8		xpeq12 5134	. . . . . 6 $/\$
9	8	anidms 677	. . . . 5
10		id 22	. . . . 5
11	9, 10	breq12d 4666	. . . 4
12	7, 11	imbi12d 334	. . 3
13		infxpen.2	. . . . . . . 8 $/\$ $/\$ $/\$
14		vex 3203	. . . . . . . . . . . . 13
15	14, 14	xpex 6962	. . . . . . . . . . . 12
16		simpll 790	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
17	13, 16	sylbi 207	. . . . . . . . . . . . . . . . 17
18		onss 6990	. . . . . . . . . . . . . . . . 17
19	17, 18	syl 17	. . . . . . . . . . . . . . . 16
20		xpss12 5225	. . . . . . . . . . . . . . . 16 $/\$
21	19, 19, 20	syl2anc 693	. . . . . . . . . . . . . . 15
22		leweon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
23		r0weon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
24	22, 23	r0weon 8835	. . . . . . . . . . . . . . . 16 $/\$ Se
25	24	simpli 474	. . . . . . . . . . . . . . 15
26		wess 5101	. . . . . . . . . . . . . . 15
27	21, 25, 26	mpisyl 21	. . . . . . . . . . . . . 14
28		weinxp 5186	. . . . . . . . . . . . . 14
29	27, 28	sylib 208	. . . . . . . . . . . . 13
30		infxpen.1	. . . . . . . . . . . . . 14
31		weeq1 5102	. . . . . . . . . . . . . 14
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13
33	29, 32	sylibr 224	. . . . . . . . . . . 12
34		infxpen.4	. . . . . . . . . . . . 13 OrdIso
35	34	oiiso 8442	. . . . . . . . . . . 12 $/\$
36	15, 33, 35	sylancr 695	. . . . . . . . . . 11
37		isof1o 6573	. . . . . . . . . . 11
38		f1ocnv 6149	. . . . . . . . . . 11
39		f1of1 6136	. . . . . . . . . . 11
40	36, 37, 38, 39	4syl 19	. . . . . . . . . 10
41		f1f1orn 6148	. . . . . . . . . 10
42	15	f1oen 7976	. . . . . . . . . 10
43	40, 41, 42	3syl 18	. . . . . . . . 9
44		f1ofn 6138	. . . . . . . . . . 11
45	36, 37, 38, 44	4syl 19	. . . . . . . . . 10
46	36	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
47	37, 38, 39	3syl 18	. . . . . . . . . . . . . . . . . 18
48		cnvimass 5485	. . . . . . . . . . . . . . . . . . 19
49		inss2 3834	. . . . . . . . . . . . . . . . . . . . . 22
50	30, 49	eqsstri 3635	. . . . . . . . . . . . . . . . . . . . 21
51		dmss 5323	. . . . . . . . . . . . . . . . . . . . 21
52	50, 51	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
53		dmxpid 5345	. . . . . . . . . . . . . . . . . . . 20
54	52, 53	sseqtri 3637	. . . . . . . . . . . . . . . . . . 19
55	48, 54	sstri 3612	. . . . . . . . . . . . . . . . . 18
56		f1ores 6151	. . . . . . . . . . . . . . . . . 18 $/\$
57	47, 55, 56	sylancl 694	. . . . . . . . . . . . . . . . 17
58	15, 15	xpex 6962	. . . . . . . . . . . . . . . . . . . . . 22
59	58	inex2 4800	. . . . . . . . . . . . . . . . . . . . 21
60	30, 59	eqeltri 2697	. . . . . . . . . . . . . . . . . . . 20
61	60	cnvex 7113	. . . . . . . . . . . . . . . . . . 19
62	61	imaex 7104	. . . . . . . . . . . . . . . . . 18
63	62	f1oen 7976	. . . . . . . . . . . . . . . . 17
64	46, 57, 63	3syl 18	. . . . . . . . . . . . . . . 16 $/\$
65		sseqin2 3817	. . . . . . . . . . . . . . . . . . 19
66	55, 65	mpbi 220	. . . . . . . . . . . . . . . . . 18
67	66	imaeq2i 5464	. . . . . . . . . . . . . . . . 17
68		isocnv 6580	. . . . . . . . . . . . . . . . . . . 20
69	46, 68	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$
70		simpr 477	. . . . . . . . . . . . . . . . . . 19 $/\$
71		isoini 6588	. . . . . . . . . . . . . . . . . . 19 $/\$
72	69, 70, 71	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$
73		fvex 6201	. . . . . . . . . . . . . . . . . . . . 21
74	73	epini 5495	. . . . . . . . . . . . . . . . . . . 20
75	74	ineq2i 3811	. . . . . . . . . . . . . . . . . . 19
76	34	oicl 8434	. . . . . . . . . . . . . . . . . . . . 21
77		f1of 6137	. . . . . . . . . . . . . . . . . . . . . . 23
78	36, 37, 38, 77	4syl 19	. . . . . . . . . . . . . . . . . . . . . 22
79	78	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . 21 $/\$
80		ordelss 5739	. . . . . . . . . . . . . . . . . . . . 21 $/\$
81	76, 79, 80	sylancr 695	. . . . . . . . . . . . . . . . . . . 20 $/\$
82		sseqin2 3817	. . . . . . . . . . . . . . . . . . . 20
83	81, 82	sylib 208	. . . . . . . . . . . . . . . . . . 19 $/\$
84	75, 83	syl5eq 2668	. . . . . . . . . . . . . . . . . 18 $/\$
85	72, 84	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $/\$
86	67, 85	syl5eqr 2670	. . . . . . . . . . . . . . . 16 $/\$
87	64, 86	breqtrd 4679	. . . . . . . . . . . . . . 15 $/\$
88	87	ensymd 8007	. . . . . . . . . . . . . 14 $/\$
89		infxpen.3	. . . . . . . . . . . . . . . . . . 19
90		fvex 6201	. . . . . . . . . . . . . . . . . . . 20
91		fvex 6201	. . . . . . . . . . . . . . . . . . . 20
92	90, 91	unex 6956	. . . . . . . . . . . . . . . . . . 19
93	89, 92	eqeltri 2697	. . . . . . . . . . . . . . . . . 18
94	93	sucex 7011	. . . . . . . . . . . . . . . . 17
95	94, 94	xpex 6962	. . . . . . . . . . . . . . . 16
96		xpss 5226	. . . . . . . . . . . . . . . . . . . 20
97		simp3 1063	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
98		vex 3203	. . . . . . . . . . . . . . . . . . . . . . 23
99		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . 24
100	99	eliniseg 5494	. . . . . . . . . . . . . . . . . . . . . . 23
101	98, 100	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
102	97, 101	sylib 208	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
103	30	breqi 4659	. . . . . . . . . . . . . . . . . . . . . . 23
104		brin 4704	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
105	103, 104	bitri 264	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
106	105	simprbi 480	. . . . . . . . . . . . . . . . . . . . 21
107		brxp 5147	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
108	107	simplbi 476	. . . . . . . . . . . . . . . . . . . . 21
109	102, 106, 108	3syl 18	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
110	96, 109	sseldi 3601	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
111	17	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
112	111	3adant3 1081	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
113		xp1st 7198	. . . . . . . . . . . . . . . . . . . . . 22
114		onelon 5748	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
115	113, 114	sylan2 491	. . . . . . . . . . . . . . . . . . . . 21 $/\$
116	112, 109, 115	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
117		eloni 5733	. . . . . . . . . . . . . . . . . . . . . . . . . 26
118		elxp7 7201	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
119	118	simprbi 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
120		ordunel 7027	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
121	120	3expib 1268	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
122	117, 119, 121	syl2im 40	. . . . . . . . . . . . . . . . . . . . . . . . 25
123	111, 70, 122	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
124	89, 123	syl5eqel 2705	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
125		simprr 796	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
126	13, 125	sylbi 207	. . . . . . . . . . . . . . . . . . . . . . . . . 26
127		simprl 794	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
128	13, 127	sylbi 207	. . . . . . . . . . . . . . . . . . . . . . . . . 26
129		iscard 8801	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
130		cardlim 8798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
131		sseq2 3627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
132		limeq 5735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133	131, 132	bibi12d 335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
134	130, 133	mpbii 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
135	129, 134	sylbir 225	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
136	135	biimpa 501	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
137	17, 126, 128, 136	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . . . . 25
138	137	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
139		limsuc 7049	. . . . . . . . . . . . . . . . . . . . . . . 24
140	138, 139	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
141	124, 140	mpbid 222	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
142		onelon 5748	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
143	17, 141, 142	syl2an2r 876	. . . . . . . . . . . . . . . . . . . . 21 $/\$
144	143	3adant3 1081	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
145		ssun1 3776	. . . . . . . . . . . . . . . . . . . . 21
146	145	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
147	105	simplbi 476	. . . . . . . . . . . . . . . . . . . . 21
148		df-br 4654	. . . . . . . . . . . . . . . . . . . . . . . . . 26
149	23	eleq2i 2693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$
150		opabid 4982	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
151	148, 149, 150	3bitri 286	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\/$ $/\$
152	151	simprbi 480	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$ $/\$
153		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
154	153	orim2i 540	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$ $/\$ $\/$
155	152, 154	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
156		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . 25
157		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . 25
158	156, 157	unex 6956	. . . . . . . . . . . . . . . . . . . . . . . 24
159	158	elsuc 5794	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
160	155, 159	sylibr 224	. . . . . . . . . . . . . . . . . . . . . 22
161		suceq 5790	. . . . . . . . . . . . . . . . . . . . . . 23
162	89, 161	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
163	160, 162	syl6eleqr 2712	. . . . . . . . . . . . . . . . . . . . 21
164	102, 147, 163	3syl 18	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
165		ontr2 5772	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
166	165	imp 445	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
167	116, 144, 146, 164, 166	syl22anc 1327	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
168		xp2nd 7199	. . . . . . . . . . . . . . . . . . . . . 22
169		onelon 5748	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
170	168, 169	sylan2 491	. . . . . . . . . . . . . . . . . . . . 21 $/\$
171	112, 109, 170	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
172		ssun2 3777	. . . . . . . . . . . . . . . . . . . . 21
173	172	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
174		ontr2 5772	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
175	174	imp 445	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
176	171, 144, 173, 164, 175	syl22anc 1327	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
177		elxp7 7201	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
178	177	biimpri 218	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
179	110, 167, 176, 178	syl12anc 1324	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
180	179	3expia 1267	. . . . . . . . . . . . . . . . 17 $/\$
181	180	ssrdv 3609	. . . . . . . . . . . . . . . 16 $/\$
182		ssdomg 8001	. . . . . . . . . . . . . . . 16
183	95, 181, 182	mpsyl 68	. . . . . . . . . . . . . . 15 $/\$
184	128	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
185		nnfi 8153	. . . . . . . . . . . . . . . . . . . 20
186		xpfi 8231	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
187	186	anidms 677	. . . . . . . . . . . . . . . . . . . . 21
188		isfinite 8549	. . . . . . . . . . . . . . . . . . . . 21
189	187, 188	sylib 208	. . . . . . . . . . . . . . . . . . . 20
190	185, 189	syl 17	. . . . . . . . . . . . . . . . . . 19
191		ssdomg 8001	. . . . . . . . . . . . . . . . . . . 20
192	14, 191	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
193		sdomdomtr 8093	. . . . . . . . . . . . . . . . . . 19 $/\$
194	190, 192, 193	syl2an 494	. . . . . . . . . . . . . . . . . 18 $/\$
195	194	expcom 451	. . . . . . . . . . . . . . . . 17
196	184, 195	syl 17	. . . . . . . . . . . . . . . 16 $/\$
197	126	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
198		breq1 4656	. . . . . . . . . . . . . . . . . . 19
199	198	rspccv 3306	. . . . . . . . . . . . . . . . . 18
200	197, 141, 199	sylc 65	. . . . . . . . . . . . . . . . 17 $/\$
201		omelon 8543	. . . . . . . . . . . . . . . . . . 19
202		ontri1 5757	. . . . . . . . . . . . . . . . . . 19 $/\$
203	201, 143, 202	sylancr 695	. . . . . . . . . . . . . . . . . 18 $/\$
204		simplr 792	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
205	13, 204	sylbi 207	. . . . . . . . . . . . . . . . . . . 20
206	205	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
207		sseq2 3627	. . . . . . . . . . . . . . . . . . . . 21
208		xpeq12 5134	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
209	208	anidms 677	. . . . . . . . . . . . . . . . . . . . . 22
210		id 22	. . . . . . . . . . . . . . . . . . . . . 22
211	209, 210	breq12d 4666	. . . . . . . . . . . . . . . . . . . . 21
212	207, 211	imbi12d 334	. . . . . . . . . . . . . . . . . . . 20
213	212	rspccv 3306	. . . . . . . . . . . . . . . . . . 19
214	206, 141, 213	sylc 65	. . . . . . . . . . . . . . . . . 18 $/\$
215	203, 214	sylbird 250	. . . . . . . . . . . . . . . . 17 $/\$
216		ensdomtr 8096	. . . . . . . . . . . . . . . . . 18 $/\$
217	216	expcom 451	. . . . . . . . . . . . . . . . 17
218	200, 215, 217	sylsyld 61	. . . . . . . . . . . . . . . 16 $/\$
219	196, 218	pm2.61d 170	. . . . . . . . . . . . . . 15 $/\$
220		domsdomtr 8095	. . . . . . . . . . . . . . 15 $/\$
221	183, 219, 220	syl2anc 693	. . . . . . . . . . . . . 14 $/\$
222		ensdomtr 8096	. . . . . . . . . . . . . 14 $/\$
223	88, 221, 222	syl2anc 693	. . . . . . . . . . . . 13 $/\$
224		ordelon 5747	. . . . . . . . . . . . . . 15 $/\$
225	76, 79, 224	sylancr 695	. . . . . . . . . . . . . 14 $/\$
226		onenon 8775	. . . . . . . . . . . . . . 15
227	111, 226	syl 17	. . . . . . . . . . . . . 14 $/\$
228		cardsdomel 8800	. . . . . . . . . . . . . 14 $/\$
229	225, 227, 228	syl2anc 693	. . . . . . . . . . . . 13 $/\$
230	223, 229	mpbid 222	. . . . . . . . . . . 12 $/\$
231		eleq2 2690	. . . . . . . . . . . . . 14
232	129, 231	sylbir 225	. . . . . . . . . . . . 13 $/\$
233	17, 197, 232	syl2an2r 876	. . . . . . . . . . . 12 $/\$
234	230, 233	mpbid 222	. . . . . . . . . . 11 $/\$
235	234	ralrimiva 2966	. . . . . . . . . 10
236		fnfvrnss 6390	. . . . . . . . . . 11 $/\$
237		ssdomg 8001	. . . . . . . . . . 11
238	14, 236, 237	mpsyl 68	. . . . . . . . . 10 $/\$
239	45, 235, 238	syl2anc 693	. . . . . . . . 9
240		endomtr 8014	. . . . . . . . 9 $/\$
241	43, 239, 240	syl2anc 693	. . . . . . . 8
242	13, 241	sylbir 225	. . . . . . 7 $/\$ $/\$ $/\$
243		df1o2 7572	. . . . . . . . . . . 12
244		1onn 7719	. . . . . . . . . . . 12
245	243, 244	eqeltrri 2698	. . . . . . . . . . 11
246		nnsdom 8551	. . . . . . . . . . 11
247		sdomdom 7983	. . . . . . . . . . 11
248	245, 246, 247	mp2b 10	. . . . . . . . . 10
249		domtr 8009	. . . . . . . . . 10 $/\$
250	248, 192, 249	sylancr 695	. . . . . . . . 9
251		0ex 4790	. . . . . . . . . . . 12
252	14, 251	xpsnen 8044	. . . . . . . . . . 11
253	252	ensymi 8006	. . . . . . . . . 10
254	14	xpdom2 8055	. . . . . . . . . 10
255		endomtr 8014	. . . . . . . . . 10 $/\$
256	253, 254, 255	sylancr 695	. . . . . . . . 9
257	250, 256	syl 17	. . . . . . . 8
258	257	ad2antrl 764	. . . . . . 7 $/\$ $/\$ $/\$
259		sbth 8080	. . . . . . 7 $/\$
260	242, 258, 259	syl2anc 693	. . . . . 6 $/\$ $/\$ $/\$
261	260	expr 643	. . . . 5 $/\$ $/\$
262		simplr 792	. . . . . . . 8 $/\$ $/\$ $/\$
263		simpll 790	. . . . . . . . 9 $/\$ $/\$ $/\$
264		simprr 796	. . . . . . . . 9 $/\$ $/\$ $/\$
265		rexnal 2995	. . . . . . . . . 10
266		onelss 5766	. . . . . . . . . . . . 13
267		ssdomg 8001	. . . . . . . . . . . . 13
268	266, 267	syld 47	. . . . . . . . . . . 12
269		bren2 7986	. . . . . . . . . . . . 13 $/\$
270	269	simplbi2 655	. . . . . . . . . . . 12
271	268, 270	syl6 35	. . . . . . . . . . 11
272	271	reximdvai 3015	. . . . . . . . . 10
273	265, 272	syl5bir 233	. . . . . . . . 9
274	263, 264, 273	sylc 65	. . . . . . . 8 $/\$ $/\$ $/\$
275		r19.29 3072	. . . . . . . 8 $/\$ $/\$
276	262, 274, 275	syl2anc 693	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
277		simprl 794	. . . . . . . 8 $/\$ $/\$ $/\$
278		onelon 5748	. . . . . . . . . . . . . . . . 17 $/\$
279		ensym 8005	. . . . . . . . . . . . . . . . . 18
280		domentr 8015	. . . . . . . . . . . . . . . . . 18 $/\$
281	192, 279, 280	syl2an 494	. . . . . . . . . . . . . . . . 17 $/\$
282		domnsym 8086	. . . . . . . . . . . . . . . . . . 19
283		nnsdom 8551	. . . . . . . . . . . . . . . . . . 19
284	282, 283	nsyl 135	. . . . . . . . . . . . . . . . . 18
285		ontri1 5757	. . . . . . . . . . . . . . . . . . 19 $/\$
286	201, 285	mpan 706	. . . . . . . . . . . . . . . . . 18
287	284, 286	syl5ibr 236	. . . . . . . . . . . . . . . . 17
288	278, 281, 287	syl2im 40	. . . . . . . . . . . . . . . 16 $/\$ $/\$
289	288	expd 452	. . . . . . . . . . . . . . 15 $/\$
290	289	impcom 446	. . . . . . . . . . . . . 14 $/\$ $/\$
291	290	imim1d 82	. . . . . . . . . . . . 13 $/\$ $/\$
292	291	imp32 449	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
293		entr 8008	. . . . . . . . . . . . . . . 16 $/\$
294	293	ancoms 469	. . . . . . . . . . . . . . 15 $/\$
295		xpen 8123	. . . . . . . . . . . . . . . . 17 $/\$
296	295	anidms 677	. . . . . . . . . . . . . . . 16
297		entr 8008	. . . . . . . . . . . . . . . 16 $/\$
298	296, 297	sylan 488	. . . . . . . . . . . . . . 15 $/\$
299	279, 294, 298	syl2an2r 876	. . . . . . . . . . . . . 14 $/\$
300	299	ex 450	. . . . . . . . . . . . 13
301	300	ad2antll 765	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
302	292, 301	mpd 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
303	302	ex 450	. . . . . . . . . 10 $/\$ $/\$ $/\$
304	303	expr 643	. . . . . . . . 9 $/\$ $/\$
305	304	rexlimdv 3030	. . . . . . . 8 $/\$ $/\$
306	277, 263, 305	syl2anc 693	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
307	276, 306	mpd 15	. . . . . 6 $/\$ $/\$ $/\$
308	307	expr 643	. . . . 5 $/\$ $/\$
309	261, 308	pm2.61d 170	. . . 4 $/\$ $/\$
310	309	exp31 630	. . 3
311	6, 12, 310	tfis3 7057	. 2
312	311	imp 445	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

wral 2912

wrex 2913

cvv 3200

cun 3572

cin 3573

wss 3574

c0 3915

csn 4177

cop 4183 class class class wbr 4653

copab 4712

cep 5028 Se wse 5071

wwe 5072

cxp 5112

ccnv 5113

cdm 5114

crn 5115

cres 5116

cima 5117

word 5722

con0 5723

wlim 5724

csuc 5725

wfn 5883

wf 5884

wf1 5885

wf1o 5887

cfv 5888

wiso 5889

com 7065

c1st 7166

c2nd 7167

c1o 7553

cen 7952

cdom 7953

csdm 7954

cfn 7955 OrdIsocoi 8414

ccrd 8761

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

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-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-uni 4437 df-int 4476 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-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-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-oi 8415 df-card 8765

This theorem is referenced by: infxpen 8837

W3C validator