infxpenlem - Metamath Proof Explorer

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

Theorem infxpenlem 8172

Description: Lemma for infxpen 8173. (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 3373	. . . 4
2		xpeq12 4854	. . . . . 6 $/\$
3	2	anidms 645	. . . . 5
4		id 22	. . . . 5
5	3, 4	breq12d 4300	. . . 4
6	1, 5	imbi12d 320	. . 3
7		sseq2 3373	. . . 4
8		xpeq12 4854	. . . . . 6 $/\$
9	8	anidms 645	. . . . 5
10		id 22	. . . . 5
11	9, 10	breq12d 4300	. . . 4
12	7, 11	imbi12d 320	. . 3
13		infxpen.2	. . . . . . . 8 $/\$ $/\$ $/\$
14		vex 2970	. . . . . . . . . . . . 13
15	14, 14	xpex 6503	. . . . . . . . . . . 12
16		simpll 753	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
17	13, 16	sylbi 195	. . . . . . . . . . . . . . . . 17
18		onss 6397	. . . . . . . . . . . . . . . . 17
19	17, 18	syl 16	. . . . . . . . . . . . . . . 16
20		xpss12 4940	. . . . . . . . . . . . . . . 16 $/\$
21	19, 19, 20	syl2anc 661	. . . . . . . . . . . . . . 15
22		leweon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
23		r0weon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
24	22, 23	r0weon 8171	. . . . . . . . . . . . . . . 16 $/\$ Se
25	24	simpli 458	. . . . . . . . . . . . . . 15
26		wess 4702	. . . . . . . . . . . . . . 15
27	21, 25, 26	mpisyl 18	. . . . . . . . . . . . . 14
28		weinxp 4901	. . . . . . . . . . . . . 14
29	27, 28	sylib 196	. . . . . . . . . . . . 13
30		infxpen.1	. . . . . . . . . . . . . 14
31		weeq1 4703	. . . . . . . . . . . . . 14
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13
33	29, 32	sylibr 212	. . . . . . . . . . . 12
34		infxpen.4	. . . . . . . . . . . . 13 OrdIso
35	34	oiiso 7743	. . . . . . . . . . . 12 $/\$
36	15, 33, 35	sylancr 663	. . . . . . . . . . 11
37		isof1o 6011	. . . . . . . . . . 11
38		f1ocnv 5648	. . . . . . . . . . 11
39		f1of1 5635	. . . . . . . . . . 11
40	36, 37, 38, 39	4syl 21	. . . . . . . . . 10
41		f1f1orn 5647	. . . . . . . . . 10
42	15	f1oen 7322	. . . . . . . . . 10
43	40, 41, 42	3syl 20	. . . . . . . . 9
44		f1ofn 5637	. . . . . . . . . . 11
45	36, 37, 38, 44	4syl 21	. . . . . . . . . 10
46	36	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
47	37, 38, 39	3syl 20	. . . . . . . . . . . . . . . . . 18
48		cnvimass 5184	. . . . . . . . . . . . . . . . . . 19
49		inss2 3566	. . . . . . . . . . . . . . . . . . . . . 22
50	30, 49	eqsstri 3381	. . . . . . . . . . . . . . . . . . . . 21
51		dmss 5034	. . . . . . . . . . . . . . . . . . . . 21
52	50, 51	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
53		dmxpid 5054	. . . . . . . . . . . . . . . . . . . 20
54	52, 53	sseqtri 3383	. . . . . . . . . . . . . . . . . . 19
55	48, 54	sstri 3360	. . . . . . . . . . . . . . . . . 18
56		f1ores 5650	. . . . . . . . . . . . . . . . . 18 $/\$
57	47, 55, 56	sylancl 662	. . . . . . . . . . . . . . . . 17
58	15, 15	xpex 6503	. . . . . . . . . . . . . . . . . . . . . 22
59	58	inex2 4429	. . . . . . . . . . . . . . . . . . . . 21
60	30, 59	eqeltri 2508	. . . . . . . . . . . . . . . . . . . 20
61	60	cnvex 6520	. . . . . . . . . . . . . . . . . . 19
62		imaexg 6510	. . . . . . . . . . . . . . . . . . 19
63	61, 62	ax-mp 5	. . . . . . . . . . . . . . . . . 18
64	63	f1oen 7322	. . . . . . . . . . . . . . . . 17
65	46, 57, 64	3syl 20	. . . . . . . . . . . . . . . 16 $/\$
66		sseqin2 3564	. . . . . . . . . . . . . . . . . . 19
67	55, 66	mpbi 208	. . . . . . . . . . . . . . . . . 18
68	67	imaeq2i 5162	. . . . . . . . . . . . . . . . 17
69		isocnv 6016	. . . . . . . . . . . . . . . . . . . 20
70	46, 69	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$
71		simpr 461	. . . . . . . . . . . . . . . . . . 19 $/\$
72		isoini 6024	. . . . . . . . . . . . . . . . . . 19 $/\$
73	70, 71, 72	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$
74		fvex 5696	. . . . . . . . . . . . . . . . . . . . 21
75	74	epini 5194	. . . . . . . . . . . . . . . . . . . 20
76	75	ineq2i 3544	. . . . . . . . . . . . . . . . . . 19
77	34	oicl 7735	. . . . . . . . . . . . . . . . . . . . 21
78		f1of 5636	. . . . . . . . . . . . . . . . . . . . . . 23
79	36, 37, 38, 78	4syl 21	. . . . . . . . . . . . . . . . . . . . . 22
80	79	ffvelrnda 5838	. . . . . . . . . . . . . . . . . . . . 21 $/\$
81		ordelss 4730	. . . . . . . . . . . . . . . . . . . . 21 $/\$
82	77, 80, 81	sylancr 663	. . . . . . . . . . . . . . . . . . . 20 $/\$
83		dfss1 3550	. . . . . . . . . . . . . . . . . . . 20
84	82, 83	sylib 196	. . . . . . . . . . . . . . . . . . 19 $/\$
85	76, 84	syl5eq 2482	. . . . . . . . . . . . . . . . . 18 $/\$
86	73, 85	eqtrd 2470	. . . . . . . . . . . . . . . . 17 $/\$
87	68, 86	syl5eqr 2484	. . . . . . . . . . . . . . . 16 $/\$
88	65, 87	breqtrd 4311	. . . . . . . . . . . . . . 15 $/\$
89	88	ensymd 7352	. . . . . . . . . . . . . 14 $/\$
90		infxpen.3	. . . . . . . . . . . . . . . . . . 19
91		fvex 5696	. . . . . . . . . . . . . . . . . . . 20
92		fvex 5696	. . . . . . . . . . . . . . . . . . . 20
93	91, 92	unex 6373	. . . . . . . . . . . . . . . . . . 19
94	90, 93	eqeltri 2508	. . . . . . . . . . . . . . . . . 18
95	94	sucex 6417	. . . . . . . . . . . . . . . . 17
96	95, 95	xpex 6503	. . . . . . . . . . . . . . . 16
97		xpss 4941	. . . . . . . . . . . . . . . . . . . 20
98		simp3 990	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
99		vex 2970	. . . . . . . . . . . . . . . . . . . . . . 23
100		vex 2970	. . . . . . . . . . . . . . . . . . . . . . . 24
101	100	eliniseg 5193	. . . . . . . . . . . . . . . . . . . . . . 23
102	99, 101	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
103	98, 102	sylib 196	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
104	30	breqi 4293	. . . . . . . . . . . . . . . . . . . . . . 23
105		brin 4336	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
106	104, 105	bitri 249	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
107	106	simprbi 464	. . . . . . . . . . . . . . . . . . . . 21
108		brxp 4865	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
109	108	simplbi 460	. . . . . . . . . . . . . . . . . . . . 21
110	103, 107, 109	3syl 20	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
111	97, 110	sseldi 3349	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
112	17	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
113	112	3adant3 1008	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
114		xp1st 6601	. . . . . . . . . . . . . . . . . . . . . 22
115		onelon 4739	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
116	114, 115	sylan2 474	. . . . . . . . . . . . . . . . . . . . 21 $/\$
117	113, 110, 116	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
118		eloni 4724	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119		elxp7 6604	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
120	119	simprbi 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
121		ordunel 6433	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
122	121	3expib 1190	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
123	118, 120, 122	syl2im 38	. . . . . . . . . . . . . . . . . . . . . . . . 25
124	112, 71, 123	sylc 60	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
125	90, 124	syl5eqel 2522	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
126		simprr 756	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
127	13, 126	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
128		simprl 755	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
129	13, 128	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130		iscard 8137	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131		cardlim 8134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
132		sseq2 3373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133		limeq 4726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
134	132, 133	bibi12d 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
135	131, 134	mpbii 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136	130, 135	sylbir 213	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
137	136	biimpa 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
138	17, 127, 129, 137	syl21anc 1217	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	138	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
140		limsuc 6455	. . . . . . . . . . . . . . . . . . . . . . . 24
141	139, 140	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
142	125, 141	mpbid 210	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
143		onelon 4739	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
144	112, 142, 143	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$
145	144	3adant3 1008	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
146		ssun1 3514	. . . . . . . . . . . . . . . . . . . . 21
147	146	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
148	106	simplbi 460	. . . . . . . . . . . . . . . . . . . . 21
149		df-br 4288	. . . . . . . . . . . . . . . . . . . . . . . . . 26
150	23	eleq2i 2502	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$
151		opabid 4591	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
152	149, 150, 151	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\/$ $/\$
153	152	simprbi 464	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$ $/\$
154		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
155	154	orim2i 518	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$ $/\$ $\/$
156	153, 155	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
157		fvex 5696	. . . . . . . . . . . . . . . . . . . . . . . . 25
158		fvex 5696	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	157, 158	unex 6373	. . . . . . . . . . . . . . . . . . . . . . . 24
160	159	elsuc 4783	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
161	156, 160	sylibr 212	. . . . . . . . . . . . . . . . . . . . . 22
162		suceq 4779	. . . . . . . . . . . . . . . . . . . . . . 23
163	90, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
164	161, 163	syl6eleqr 2529	. . . . . . . . . . . . . . . . . . . . 21
165	103, 148, 164	3syl 20	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
166		ontr2 4761	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
167	166	imp 429	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
168	117, 145, 147, 165, 167	syl22anc 1219	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
169		xp2nd 6602	. . . . . . . . . . . . . . . . . . . . . 22
170		onelon 4739	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
171	169, 170	sylan2 474	. . . . . . . . . . . . . . . . . . . . 21 $/\$
172	113, 110, 171	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
173		ssun2 3515	. . . . . . . . . . . . . . . . . . . . 21
174	173	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
175		ontr2 4761	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
176	175	imp 429	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
177	172, 145, 174, 165, 176	syl22anc 1219	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
178		elxp7 6604	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
179	178	biimpri 206	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
180	111, 168, 177, 179	syl12anc 1216	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
181	180	3expia 1189	. . . . . . . . . . . . . . . . 17 $/\$
182	181	ssrdv 3357	. . . . . . . . . . . . . . . 16 $/\$
183		ssdomg 7347	. . . . . . . . . . . . . . . 16
184	96, 182, 183	mpsyl 63	. . . . . . . . . . . . . . 15 $/\$
185	129	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
186		nnfi 7495	. . . . . . . . . . . . . . . . . . . 20
187		xpfi 7575	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
188	187	anidms 645	. . . . . . . . . . . . . . . . . . . . 21
189		isfinite 7850	. . . . . . . . . . . . . . . . . . . . 21
190	188, 189	sylib 196	. . . . . . . . . . . . . . . . . . . 20
191	186, 190	syl 16	. . . . . . . . . . . . . . . . . . 19
192		ssdomg 7347	. . . . . . . . . . . . . . . . . . . 20
193	14, 192	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
194		sdomdomtr 7436	. . . . . . . . . . . . . . . . . . 19 $/\$
195	191, 193, 194	syl2an 477	. . . . . . . . . . . . . . . . . 18 $/\$
196	195	expcom 435	. . . . . . . . . . . . . . . . 17
197	185, 196	syl 16	. . . . . . . . . . . . . . . 16 $/\$
198	127	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
199		breq1 4290	. . . . . . . . . . . . . . . . . . 19
200	199	rspccv 3065	. . . . . . . . . . . . . . . . . 18
201	198, 142, 200	sylc 60	. . . . . . . . . . . . . . . . 17 $/\$
202		omelon 7844	. . . . . . . . . . . . . . . . . . 19
203		ontri1 4748	. . . . . . . . . . . . . . . . . . 19 $/\$
204	202, 144, 203	sylancr 663	. . . . . . . . . . . . . . . . . 18 $/\$
205		simplr 754	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
206	13, 205	sylbi 195	. . . . . . . . . . . . . . . . . . . 20
207	206	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
208		sseq2 3373	. . . . . . . . . . . . . . . . . . . . 21
209		xpeq12 4854	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
210	209	anidms 645	. . . . . . . . . . . . . . . . . . . . . 22
211		id 22	. . . . . . . . . . . . . . . . . . . . . 22
212	210, 211	breq12d 4300	. . . . . . . . . . . . . . . . . . . . 21
213	208, 212	imbi12d 320	. . . . . . . . . . . . . . . . . . . 20
214	213	rspccv 3065	. . . . . . . . . . . . . . . . . . 19
215	207, 142, 214	sylc 60	. . . . . . . . . . . . . . . . . 18 $/\$
216	204, 215	sylbird 235	. . . . . . . . . . . . . . . . 17 $/\$
217		ensdomtr 7439	. . . . . . . . . . . . . . . . . 18 $/\$
218	217	expcom 435	. . . . . . . . . . . . . . . . 17
219	201, 216, 218	sylsyld 56	. . . . . . . . . . . . . . . 16 $/\$
220	197, 219	pm2.61d 158	. . . . . . . . . . . . . . 15 $/\$
221		domsdomtr 7438	. . . . . . . . . . . . . . 15 $/\$
222	184, 220, 221	syl2anc 661	. . . . . . . . . . . . . 14 $/\$
223		ensdomtr 7439	. . . . . . . . . . . . . 14 $/\$
224	89, 222, 223	syl2anc 661	. . . . . . . . . . . . 13 $/\$
225		ordelon 4738	. . . . . . . . . . . . . . 15 $/\$
226	77, 80, 225	sylancr 663	. . . . . . . . . . . . . 14 $/\$
227		onenon 8111	. . . . . . . . . . . . . . 15
228	112, 227	syl 16	. . . . . . . . . . . . . 14 $/\$
229		cardsdomel 8136	. . . . . . . . . . . . . 14 $/\$
230	226, 228, 229	syl2anc 661	. . . . . . . . . . . . 13 $/\$
231	224, 230	mpbid 210	. . . . . . . . . . . 12 $/\$
232		eleq2 2499	. . . . . . . . . . . . . 14
233	130, 232	sylbir 213	. . . . . . . . . . . . 13 $/\$
234	112, 198, 233	syl2anc 661	. . . . . . . . . . . 12 $/\$
235	231, 234	mpbid 210	. . . . . . . . . . 11 $/\$
236	235	ralrimiva 2794	. . . . . . . . . 10
237		fnfvrnss 5866	. . . . . . . . . . 11 $/\$
238		ssdomg 7347	. . . . . . . . . . 11
239	14, 237, 238	mpsyl 63	. . . . . . . . . 10 $/\$
240	45, 236, 239	syl2anc 661	. . . . . . . . 9
241		endomtr 7359	. . . . . . . . 9 $/\$
242	43, 240, 241	syl2anc 661	. . . . . . . 8
243	13, 242	sylbir 213	. . . . . . 7 $/\$ $/\$ $/\$
244		df1o2 6924	. . . . . . . . . . . 12
245		1onn 7070	. . . . . . . . . . . 12
246	244, 245	eqeltrri 2509	. . . . . . . . . . 11
247		nnsdom 7851	. . . . . . . . . . 11
248		sdomdom 7329	. . . . . . . . . . 11
249	246, 247, 248	mp2b 10	. . . . . . . . . 10
250		domtr 7354	. . . . . . . . . 10 $/\$
251	249, 193, 250	sylancr 663	. . . . . . . . 9
252		0ex 4417	. . . . . . . . . . . 12
253	14, 252	xpsnen 7387	. . . . . . . . . . 11
254	253	ensymi 7351	. . . . . . . . . 10
255	14	xpdom2 7398	. . . . . . . . . 10
256		endomtr 7359	. . . . . . . . . 10 $/\$
257	254, 255, 256	sylancr 663	. . . . . . . . 9
258	251, 257	syl 16	. . . . . . . 8
259	258	ad2antrl 727	. . . . . . 7 $/\$ $/\$ $/\$
260		sbth 7423	. . . . . . 7 $/\$
261	243, 259, 260	syl2anc 661	. . . . . 6 $/\$ $/\$ $/\$
262	261	expr 615	. . . . 5 $/\$ $/\$
263		simplr 754	. . . . . . . 8 $/\$ $/\$ $/\$
264		simpll 753	. . . . . . . . 9 $/\$ $/\$ $/\$
265		simprr 756	. . . . . . . . 9 $/\$ $/\$ $/\$
266		rexnal 2721	. . . . . . . . . 10
267		onelss 4756	. . . . . . . . . . . . 13
268		ssdomg 7347	. . . . . . . . . . . . 13
269	267, 268	syld 44	. . . . . . . . . . . 12
270		bren2 7332	. . . . . . . . . . . . 13 $/\$
271	270	simplbi2 625	. . . . . . . . . . . 12
272	269, 271	syl6 33	. . . . . . . . . . 11
273	272	reximdvai 2821	. . . . . . . . . 10
274	266, 273	syl5bir 218	. . . . . . . . 9
275	264, 265, 274	sylc 60	. . . . . . . 8 $/\$ $/\$ $/\$
276		r19.29 2852	. . . . . . . 8 $/\$ $/\$
277	263, 275, 276	syl2anc 661	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
278		simprl 755	. . . . . . . 8 $/\$ $/\$ $/\$
279		onelon 4739	. . . . . . . . . . . . . . . . 17 $/\$
280		ensym 7350	. . . . . . . . . . . . . . . . . 18
281		domentr 7360	. . . . . . . . . . . . . . . . . 18 $/\$
282	193, 280, 281	syl2an 477	. . . . . . . . . . . . . . . . 17 $/\$
283		domnsym 7429	. . . . . . . . . . . . . . . . . . 19
284		nnsdom 7851	. . . . . . . . . . . . . . . . . . 19
285	283, 284	nsyl 121	. . . . . . . . . . . . . . . . . 18
286		ontri1 4748	. . . . . . . . . . . . . . . . . . 19 $/\$
287	202, 286	mpan 670	. . . . . . . . . . . . . . . . . 18
288	285, 287	syl5ibr 221	. . . . . . . . . . . . . . . . 17
289	279, 282, 288	syl2im 38	. . . . . . . . . . . . . . . 16 $/\$ $/\$
290	289	expd 436	. . . . . . . . . . . . . . 15 $/\$
291	290	impcom 430	. . . . . . . . . . . . . 14 $/\$ $/\$
292	291	imim1d 75	. . . . . . . . . . . . 13 $/\$ $/\$
293	292	imp32 433	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
294		entr 7353	. . . . . . . . . . . . . . . 16 $/\$
295	294	ancoms 453	. . . . . . . . . . . . . . 15 $/\$
296		xpen 7466	. . . . . . . . . . . . . . . . . 18 $/\$
297	296	anidms 645	. . . . . . . . . . . . . . . . 17
298		entr 7353	. . . . . . . . . . . . . . . . 17 $/\$
299	297, 298	sylan 471	. . . . . . . . . . . . . . . 16 $/\$
300	280, 299	sylan 471	. . . . . . . . . . . . . . 15 $/\$
301	295, 300	syldan 470	. . . . . . . . . . . . . 14 $/\$
302	301	ex 434	. . . . . . . . . . . . 13
303	302	ad2antll 728	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
304	293, 303	mpd 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
305	304	ex 434	. . . . . . . . . 10 $/\$ $/\$ $/\$
306	305	expr 615	. . . . . . . . 9 $/\$ $/\$
307	306	rexlimdv 2835	. . . . . . . 8 $/\$ $/\$
308	278, 264, 307	syl2anc 661	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
309	277, 308	mpd 15	. . . . . 6 $/\$ $/\$ $/\$
310	309	expr 615	. . . . 5 $/\$ $/\$
311	262, 310	pm2.61d 158	. . . 4 $/\$ $/\$
312	311	exp31 604	. . 3
313	6, 12, 312	tfis3 6463	. 2
314	313	imp 429	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wcel 1756

wral 2710

wrex 2711

cvv 2967

cun 3321

cin 3322

wss 3323

c0 3632

csn 3872

cop 3878 class class class wbr 4287

copab 4344

cep 4625 Se wse 4672

wwe 4673

word 4713

con0 4714

wlim 4715

csuc 4716

cxp 4833

ccnv 4834

cdm 4835

crn 4836

cres 4837

cima 4838

wfn 5408

wf 5409

wf1 5410

wf1o 5412

cfv 5413

wiso 5414

com 6471

c1st 6570

c2nd 6571

c1o 6905

cen 7299

cdom 7300

csdm 7301

cfn 7302 OrdIsocoi 7715

ccrd 8097

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-inf2 7839

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-se 4675 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-om 6472 df-1st 6572 df-2nd 6573 df-recs 6824 df-rdg 6858 df-1o 6912 df-oadd 6916 df-er 7093 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-oi 7716 df-card 8101

This theorem is referenced by: infxpen 8173

W3C validator