infxpenlem - Metamath Proof Explorer

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

Theorem infxpenlem 8446

Description: Lemma for infxpen 8447. (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 3486	. . . 4
2		xpeq12 4869	. . . . . 6 $/\$
3	2	anidms 649	. . . . 5
4		id 23	. . . . 5
5	3, 4	breq12d 4433	. . . 4
6	1, 5	imbi12d 321	. . 3
7		sseq2 3486	. . . 4
8		xpeq12 4869	. . . . . 6 $/\$
9	8	anidms 649	. . . . 5
10		id 23	. . . . 5
11	9, 10	breq12d 4433	. . . 4
12	7, 11	imbi12d 321	. . 3
13		infxpen.2	. . . . . . . 8 $/\$ $/\$ $/\$
14		vex 3084	. . . . . . . . . . . . 13
15	14, 14	xpex 6606	. . . . . . . . . . . 12
16		simpll 758	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
17	13, 16	sylbi 198	. . . . . . . . . . . . . . . . 17
18		onss 6628	. . . . . . . . . . . . . . . . 17
19	17, 18	syl 17	. . . . . . . . . . . . . . . 16
20		xpss12 4956	. . . . . . . . . . . . . . . 16 $/\$
21	19, 19, 20	syl2anc 665	. . . . . . . . . . . . . . 15
22		leweon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
23		r0weon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
24	22, 23	r0weon 8445	. . . . . . . . . . . . . . . 16 $/\$ Se
25	24	simpli 459	. . . . . . . . . . . . . . 15
26		wess 4837	. . . . . . . . . . . . . . 15
27	21, 25, 26	mpisyl 22	. . . . . . . . . . . . . 14
28		weinxp 4918	. . . . . . . . . . . . . 14
29	27, 28	sylib 199	. . . . . . . . . . . . 13
30		infxpen.1	. . . . . . . . . . . . . 14
31		weeq1 4838	. . . . . . . . . . . . . 14
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13
33	29, 32	sylibr 215	. . . . . . . . . . . 12
34		infxpen.4	. . . . . . . . . . . . 13 OrdIso
35	34	oiiso 8055	. . . . . . . . . . . 12 $/\$
36	15, 33, 35	sylancr 667	. . . . . . . . . . 11
37		isof1o 6228	. . . . . . . . . . 11
38		f1ocnv 5840	. . . . . . . . . . 11
39		f1of1 5827	. . . . . . . . . . 11
40	36, 37, 38, 39	4syl 19	. . . . . . . . . 10
41		f1f1orn 5839	. . . . . . . . . 10
42	15	f1oen 7594	. . . . . . . . . 10
43	40, 41, 42	3syl 18	. . . . . . . . 9
44		f1ofn 5829	. . . . . . . . . . 11
45	36, 37, 38, 44	4syl 19	. . . . . . . . . 10
46	36	adantr 466	. . . . . . . . . . . . . . . . 17 $/\$
47	37, 38, 39	3syl 18	. . . . . . . . . . . . . . . . . 18
48		cnvimass 5204	. . . . . . . . . . . . . . . . . . 19
49		inss2 3683	. . . . . . . . . . . . . . . . . . . . . 22
50	30, 49	eqsstri 3494	. . . . . . . . . . . . . . . . . . . . 21
51		dmss 5050	. . . . . . . . . . . . . . . . . . . . 21
52	50, 51	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
53		dmxpid 5070	. . . . . . . . . . . . . . . . . . . 20
54	52, 53	sseqtri 3496	. . . . . . . . . . . . . . . . . . 19
55	48, 54	sstri 3473	. . . . . . . . . . . . . . . . . 18
56		f1ores 5842	. . . . . . . . . . . . . . . . . 18 $/\$
57	47, 55, 56	sylancl 666	. . . . . . . . . . . . . . . . 17
58	15, 15	xpex 6606	. . . . . . . . . . . . . . . . . . . . . 22
59	58	inex2 4563	. . . . . . . . . . . . . . . . . . . . 21
60	30, 59	eqeltri 2506	. . . . . . . . . . . . . . . . . . . 20
61	60	cnvex 6751	. . . . . . . . . . . . . . . . . . 19
62		imaexg 6741	. . . . . . . . . . . . . . . . . . 19
63	61, 62	ax-mp 5	. . . . . . . . . . . . . . . . . 18
64	63	f1oen 7594	. . . . . . . . . . . . . . . . 17
65	46, 57, 64	3syl 18	. . . . . . . . . . . . . . . 16 $/\$
66		sseqin2 3681	. . . . . . . . . . . . . . . . . . 19
67	55, 66	mpbi 211	. . . . . . . . . . . . . . . . . 18
68	67	imaeq2i 5182	. . . . . . . . . . . . . . . . 17
69		isocnv 6233	. . . . . . . . . . . . . . . . . . . 20
70	46, 69	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$
71		simpr 462	. . . . . . . . . . . . . . . . . . 19 $/\$
72		isoini 6241	. . . . . . . . . . . . . . . . . . 19 $/\$
73	70, 71, 72	syl2anc 665	. . . . . . . . . . . . . . . . . 18 $/\$
74		fvex 5888	. . . . . . . . . . . . . . . . . . . . 21
75	74	epini 5214	. . . . . . . . . . . . . . . . . . . 20
76	75	ineq2i 3661	. . . . . . . . . . . . . . . . . . 19
77	34	oicl 8047	. . . . . . . . . . . . . . . . . . . . 21
78		f1of 5828	. . . . . . . . . . . . . . . . . . . . . . 23
79	36, 37, 38, 78	4syl 19	. . . . . . . . . . . . . . . . . . . . . 22
80	79	ffvelrnda 6034	. . . . . . . . . . . . . . . . . . . . 21 $/\$
81		ordelss 5455	. . . . . . . . . . . . . . . . . . . . 21 $/\$
82	77, 80, 81	sylancr 667	. . . . . . . . . . . . . . . . . . . 20 $/\$
83		dfss1 3667	. . . . . . . . . . . . . . . . . . . 20
84	82, 83	sylib 199	. . . . . . . . . . . . . . . . . . 19 $/\$
85	76, 84	syl5eq 2475	. . . . . . . . . . . . . . . . . 18 $/\$
86	73, 85	eqtrd 2463	. . . . . . . . . . . . . . . . 17 $/\$
87	68, 86	syl5eqr 2477	. . . . . . . . . . . . . . . 16 $/\$
88	65, 87	breqtrd 4445	. . . . . . . . . . . . . . 15 $/\$
89	88	ensymd 7624	. . . . . . . . . . . . . 14 $/\$
90		infxpen.3	. . . . . . . . . . . . . . . . . . 19
91		fvex 5888	. . . . . . . . . . . . . . . . . . . 20
92		fvex 5888	. . . . . . . . . . . . . . . . . . . 20
93	91, 92	unex 6600	. . . . . . . . . . . . . . . . . . 19
94	90, 93	eqeltri 2506	. . . . . . . . . . . . . . . . . 18
95	94	sucex 6649	. . . . . . . . . . . . . . . . 17
96	95, 95	xpex 6606	. . . . . . . . . . . . . . . 16
97		xpss 4957	. . . . . . . . . . . . . . . . . . . 20
98		simp3 1007	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
99		vex 3084	. . . . . . . . . . . . . . . . . . . . . . 23
100		vex 3084	. . . . . . . . . . . . . . . . . . . . . . . 24
101	100	eliniseg 5213	. . . . . . . . . . . . . . . . . . . . . . 23
102	99, 101	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
103	98, 102	sylib 199	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
104	30	breqi 4426	. . . . . . . . . . . . . . . . . . . . . . 23
105		brin 4470	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
106	104, 105	bitri 252	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
107	106	simprbi 465	. . . . . . . . . . . . . . . . . . . . 21
108		brxp 4881	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
109	108	simplbi 461	. . . . . . . . . . . . . . . . . . . . 21
110	103, 107, 109	3syl 18	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
111	97, 110	sseldi 3462	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
112	17	adantr 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
113	112	3adant3 1025	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
114		xp1st 6834	. . . . . . . . . . . . . . . . . . . . . 22
115		onelon 5464	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
116	114, 115	sylan2 476	. . . . . . . . . . . . . . . . . . . . 21 $/\$
117	113, 110, 116	syl2anc 665	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
118		eloni 5449	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119		elxp7 6837	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
120	119	simprbi 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
121		ordunel 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
122	121	3expib 1208	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
123	118, 120, 122	syl2im 39	. . . . . . . . . . . . . . . . . . . . . . . . 25
124	112, 71, 123	sylc 62	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
125	90, 124	syl5eqel 2514	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
126		simprr 764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
127	13, 126	sylbi 198	. . . . . . . . . . . . . . . . . . . . . . . . . 26
128		simprl 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
129	13, 128	sylbi 198	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130		iscard 8411	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131		cardlim 8408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
132		sseq2 3486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133		limeq 5451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
134	132, 133	bibi12d 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
135	131, 134	mpbii 214	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136	130, 135	sylbir 216	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
137	136	biimpa 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
138	17, 127, 129, 137	syl21anc 1263	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	138	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
140		limsuc 6687	. . . . . . . . . . . . . . . . . . . . . . . 24
141	139, 140	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
142	125, 141	mpbid 213	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
143		onelon 5464	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
144	112, 142, 143	syl2anc 665	. . . . . . . . . . . . . . . . . . . . 21 $/\$
145	144	3adant3 1025	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
146		ssun1 3629	. . . . . . . . . . . . . . . . . . . . 21
147	146	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
148	106	simplbi 461	. . . . . . . . . . . . . . . . . . . . 21
149		df-br 4421	. . . . . . . . . . . . . . . . . . . . . . . . . 26
150	23	eleq2i 2500	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$
151		opabid 4724	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
152	149, 150, 151	3bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\/$ $/\$
153	152	simprbi 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$ $/\$
154		simpl 458	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
155	154	orim2i 520	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$ $/\$ $\/$
156	153, 155	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
157		fvex 5888	. . . . . . . . . . . . . . . . . . . . . . . . 25
158		fvex 5888	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	157, 158	unex 6600	. . . . . . . . . . . . . . . . . . . . . . . 24
160	159	elsuc 5508	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
161	156, 160	sylibr 215	. . . . . . . . . . . . . . . . . . . . . 22
162		suceq 5504	. . . . . . . . . . . . . . . . . . . . . . 23
163	90, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
164	161, 163	syl6eleqr 2521	. . . . . . . . . . . . . . . . . . . . 21
165	103, 148, 164	3syl 18	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
166		ontr2 5486	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
167	166	imp 430	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
168	117, 145, 147, 165, 167	syl22anc 1265	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
169		xp2nd 6835	. . . . . . . . . . . . . . . . . . . . . 22
170		onelon 5464	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
171	169, 170	sylan2 476	. . . . . . . . . . . . . . . . . . . . 21 $/\$
172	113, 110, 171	syl2anc 665	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
173		ssun2 3630	. . . . . . . . . . . . . . . . . . . . 21
174	173	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
175		ontr2 5486	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
176	175	imp 430	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
177	172, 145, 174, 165, 176	syl22anc 1265	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
178		elxp7 6837	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
179	178	biimpri 209	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
180	111, 168, 177, 179	syl12anc 1262	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
181	180	3expia 1207	. . . . . . . . . . . . . . . . 17 $/\$
182	181	ssrdv 3470	. . . . . . . . . . . . . . . 16 $/\$
183		ssdomg 7619	. . . . . . . . . . . . . . . 16
184	96, 182, 183	mpsyl 65	. . . . . . . . . . . . . . 15 $/\$
185	129	adantr 466	. . . . . . . . . . . . . . . . 17 $/\$
186		nnfi 7768	. . . . . . . . . . . . . . . . . . . 20
187		xpfi 7845	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
188	187	anidms 649	. . . . . . . . . . . . . . . . . . . . 21
189		isfinite 8160	. . . . . . . . . . . . . . . . . . . . 21
190	188, 189	sylib 199	. . . . . . . . . . . . . . . . . . . 20
191	186, 190	syl 17	. . . . . . . . . . . . . . . . . . 19
192		ssdomg 7619	. . . . . . . . . . . . . . . . . . . 20
193	14, 192	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
194		sdomdomtr 7708	. . . . . . . . . . . . . . . . . . 19 $/\$
195	191, 193, 194	syl2an 479	. . . . . . . . . . . . . . . . . 18 $/\$
196	195	expcom 436	. . . . . . . . . . . . . . . . 17
197	185, 196	syl 17	. . . . . . . . . . . . . . . 16 $/\$
198	127	adantr 466	. . . . . . . . . . . . . . . . . 18 $/\$
199		breq1 4423	. . . . . . . . . . . . . . . . . . 19
200	199	rspccv 3179	. . . . . . . . . . . . . . . . . 18
201	198, 142, 200	sylc 62	. . . . . . . . . . . . . . . . 17 $/\$
202		omelon 8154	. . . . . . . . . . . . . . . . . . 19
203		ontri1 5473	. . . . . . . . . . . . . . . . . . 19 $/\$
204	202, 144, 203	sylancr 667	. . . . . . . . . . . . . . . . . 18 $/\$
205		simplr 760	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
206	13, 205	sylbi 198	. . . . . . . . . . . . . . . . . . . 20
207	206	adantr 466	. . . . . . . . . . . . . . . . . . 19 $/\$
208		sseq2 3486	. . . . . . . . . . . . . . . . . . . . 21
209		xpeq12 4869	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
210	209	anidms 649	. . . . . . . . . . . . . . . . . . . . . 22
211		id 23	. . . . . . . . . . . . . . . . . . . . . 22
212	210, 211	breq12d 4433	. . . . . . . . . . . . . . . . . . . . 21
213	208, 212	imbi12d 321	. . . . . . . . . . . . . . . . . . . 20
214	213	rspccv 3179	. . . . . . . . . . . . . . . . . . 19
215	207, 142, 214	sylc 62	. . . . . . . . . . . . . . . . . 18 $/\$
216	204, 215	sylbird 238	. . . . . . . . . . . . . . . . 17 $/\$
217		ensdomtr 7711	. . . . . . . . . . . . . . . . . 18 $/\$
218	217	expcom 436	. . . . . . . . . . . . . . . . 17
219	201, 216, 218	sylsyld 58	. . . . . . . . . . . . . . . 16 $/\$
220	197, 219	pm2.61d 161	. . . . . . . . . . . . . . 15 $/\$
221		domsdomtr 7710	. . . . . . . . . . . . . . 15 $/\$
222	184, 220, 221	syl2anc 665	. . . . . . . . . . . . . 14 $/\$
223		ensdomtr 7711	. . . . . . . . . . . . . 14 $/\$
224	89, 222, 223	syl2anc 665	. . . . . . . . . . . . 13 $/\$
225		ordelon 5463	. . . . . . . . . . . . . . 15 $/\$
226	77, 80, 225	sylancr 667	. . . . . . . . . . . . . 14 $/\$
227		onenon 8385	. . . . . . . . . . . . . . 15
228	112, 227	syl 17	. . . . . . . . . . . . . 14 $/\$
229		cardsdomel 8410	. . . . . . . . . . . . . 14 $/\$
230	226, 228, 229	syl2anc 665	. . . . . . . . . . . . 13 $/\$
231	224, 230	mpbid 213	. . . . . . . . . . . 12 $/\$
232		eleq2 2495	. . . . . . . . . . . . . 14
233	130, 232	sylbir 216	. . . . . . . . . . . . 13 $/\$
234	112, 198, 233	syl2anc 665	. . . . . . . . . . . 12 $/\$
235	231, 234	mpbid 213	. . . . . . . . . . 11 $/\$
236	235	ralrimiva 2839	. . . . . . . . . 10
237		fnfvrnss 6063	. . . . . . . . . . 11 $/\$
238		ssdomg 7619	. . . . . . . . . . 11
239	14, 237, 238	mpsyl 65	. . . . . . . . . 10 $/\$
240	45, 236, 239	syl2anc 665	. . . . . . . . 9
241		endomtr 7631	. . . . . . . . 9 $/\$
242	43, 240, 241	syl2anc 665	. . . . . . . 8
243	13, 242	sylbir 216	. . . . . . 7 $/\$ $/\$ $/\$
244		df1o2 7199	. . . . . . . . . . . 12
245		1onn 7345	. . . . . . . . . . . 12
246	244, 245	eqeltrri 2507	. . . . . . . . . . 11
247		nnsdom 8161	. . . . . . . . . . 11
248		sdomdom 7601	. . . . . . . . . . 11
249	246, 247, 248	mp2b 10	. . . . . . . . . 10
250		domtr 7626	. . . . . . . . . 10 $/\$
251	249, 193, 250	sylancr 667	. . . . . . . . 9
252		0ex 4553	. . . . . . . . . . . 12
253	14, 252	xpsnen 7659	. . . . . . . . . . 11
254	253	ensymi 7623	. . . . . . . . . 10
255	14	xpdom2 7670	. . . . . . . . . 10
256		endomtr 7631	. . . . . . . . . 10 $/\$
257	254, 255, 256	sylancr 667	. . . . . . . . 9
258	251, 257	syl 17	. . . . . . . 8
259	258	ad2antrl 732	. . . . . . 7 $/\$ $/\$ $/\$
260		sbth 7695	. . . . . . 7 $/\$
261	243, 259, 260	syl2anc 665	. . . . . 6 $/\$ $/\$ $/\$
262	261	expr 618	. . . . 5 $/\$ $/\$
263		simplr 760	. . . . . . . 8 $/\$ $/\$ $/\$
264		simpll 758	. . . . . . . . 9 $/\$ $/\$ $/\$
265		simprr 764	. . . . . . . . 9 $/\$ $/\$ $/\$
266		rexnal 2873	. . . . . . . . . 10
267		onelss 5481	. . . . . . . . . . . . 13
268		ssdomg 7619	. . . . . . . . . . . . 13
269	267, 268	syld 45	. . . . . . . . . . . 12
270		bren2 7604	. . . . . . . . . . . . 13 $/\$
271	270	simplbi2 629	. . . . . . . . . . . 12
272	269, 271	syl6 34	. . . . . . . . . . 11
273	272	reximdvai 2897	. . . . . . . . . 10
274	266, 273	syl5bir 221	. . . . . . . . 9
275	264, 265, 274	sylc 62	. . . . . . . 8 $/\$ $/\$ $/\$
276		r19.29 2963	. . . . . . . 8 $/\$ $/\$
277	263, 275, 276	syl2anc 665	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
278		simprl 762	. . . . . . . 8 $/\$ $/\$ $/\$
279		onelon 5464	. . . . . . . . . . . . . . . . 17 $/\$
280		ensym 7622	. . . . . . . . . . . . . . . . . 18
281		domentr 7632	. . . . . . . . . . . . . . . . . 18 $/\$
282	193, 280, 281	syl2an 479	. . . . . . . . . . . . . . . . 17 $/\$
283		domnsym 7701	. . . . . . . . . . . . . . . . . . 19
284		nnsdom 8161	. . . . . . . . . . . . . . . . . . 19
285	283, 284	nsyl 124	. . . . . . . . . . . . . . . . . 18
286		ontri1 5473	. . . . . . . . . . . . . . . . . . 19 $/\$
287	202, 286	mpan 674	. . . . . . . . . . . . . . . . . 18
288	285, 287	syl5ibr 224	. . . . . . . . . . . . . . . . 17
289	279, 282, 288	syl2im 39	. . . . . . . . . . . . . . . 16 $/\$ $/\$
290	289	expd 437	. . . . . . . . . . . . . . 15 $/\$
291	290	impcom 431	. . . . . . . . . . . . . 14 $/\$ $/\$
292	291	imim1d 78	. . . . . . . . . . . . 13 $/\$ $/\$
293	292	imp32 434	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
294		entr 7625	. . . . . . . . . . . . . . . 16 $/\$
295	294	ancoms 454	. . . . . . . . . . . . . . 15 $/\$
296		xpen 7738	. . . . . . . . . . . . . . . . . 18 $/\$
297	296	anidms 649	. . . . . . . . . . . . . . . . 17
298		entr 7625	. . . . . . . . . . . . . . . . 17 $/\$
299	297, 298	sylan 473	. . . . . . . . . . . . . . . 16 $/\$
300	280, 299	sylan 473	. . . . . . . . . . . . . . 15 $/\$
301	295, 300	syldan 472	. . . . . . . . . . . . . 14 $/\$
302	301	ex 435	. . . . . . . . . . . . 13
303	302	ad2antll 733	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
304	293, 303	mpd 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
305	304	ex 435	. . . . . . . . . 10 $/\$ $/\$ $/\$
306	305	expr 618	. . . . . . . . 9 $/\$ $/\$
307	306	rexlimdv 2915	. . . . . . . 8 $/\$ $/\$
308	278, 264, 307	syl2anc 665	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
309	277, 308	mpd 15	. . . . . 6 $/\$ $/\$ $/\$
310	309	expr 618	. . . . 5 $/\$ $/\$
311	262, 310	pm2.61d 161	. . . 4 $/\$ $/\$
312	311	exp31 607	. . 3
313	6, 12, 312	tfis3 6695	. 2
314	313	imp 430	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1868

wral 2775

wrex 2776

cvv 3081

cun 3434

cin 3435

wss 3436

c0 3761

csn 3996

cop 4002 class class class wbr 4420

copab 4478

cep 4759 Se wse 4807

wwe 4808

cxp 4848

ccnv 4849

cdm 4850

crn 4851

cres 4852

cima 4853

word 5438

con0 5439

wlim 5440

csuc 5441

wfn 5593

wf 5594

wf1 5595

wf1o 5597

cfv 5598

wiso 5599

com 6703

c1st 6802

c2nd 6803

c1o 7180

cen 7571

cdom 7572

csdm 7573

cfn 7574 OrdIsocoi 8027

ccrd 8371

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1839 ax-8 1870 ax-9 1872 ax-10 1887 ax-11 1892 ax-12 1905 ax-13 2053 ax-ext 2400 ax-rep 4533 ax-sep 4543 ax-nul 4552 ax-pow 4599 ax-pr 4657 ax-un 6594 ax-inf2 8149

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2269 df-mo 2270 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2572 df-ne 2620 df-ral 2780 df-rex 2781 df-reu 2782 df-rmo 2783 df-rab 2784 df-v 3083 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3910 df-pw 3981 df-sn 3997 df-pr 3999 df-tp 4001 df-op 4003 df-uni 4217 df-int 4253 df-iun 4298 df-br 4421 df-opab 4480 df-mpt 4481 df-tr 4516 df-eprel 4761 df-id 4765 df-po 4771 df-so 4772 df-fr 4809 df-se 4810 df-we 4811 df-xp 4856 df-rel 4857 df-cnv 4858 df-co 4859 df-dm 4860 df-rn 4861 df-res 4862 df-ima 4863 df-pred 5396 df-ord 5442 df-on 5443 df-lim 5444 df-suc 5445 df-iota 5562 df-fun 5600 df-fn 5601 df-f 5602 df-f1 5603 df-fo 5604 df-f1o 5605 df-fv 5606 df-isom 5607 df-riota 6264 df-ov 6305 df-oprab 6306 df-mpt2 6307 df-om 6704 df-1st 6804 df-2nd 6805 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-1o 7187 df-oadd 7191 df-er 7368 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-oi 8028 df-card 8375

This theorem is referenced by: infxpen 8447

W3C validator