infxpenlem - Metamath Proof Explorer

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

Theorem infxpenlem 8170

Description: Lemma for infxpen 8171. (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 3368	. . . 4
2		xpeq12 4848	. . . . . 6 $/\$
3	2	anidms 640	. . . . 5
4		id 22	. . . . 5
5	3, 4	breq12d 4295	. . . 4
6	1, 5	imbi12d 320	. . 3
7		sseq2 3368	. . . 4
8		xpeq12 4848	. . . . . 6 $/\$
9	8	anidms 640	. . . . 5
10		id 22	. . . . 5
11	9, 10	breq12d 4295	. . . 4
12	7, 11	imbi12d 320	. . 3
13		infxpen.2	. . . . . . . 8 $/\$ $/\$ $/\$
14		vex 2967	. . . . . . . . . . . . 13
15	14, 14	xpex 6499	. . . . . . . . . . . 12
16		simpll 748	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
17	13, 16	sylbi 195	. . . . . . . . . . . . . . . . 17
18		onss 6393	. . . . . . . . . . . . . . . . 17
19	17, 18	syl 16	. . . . . . . . . . . . . . . 16
20		xpss12 4934	. . . . . . . . . . . . . . . 16 $/\$
21	19, 19, 20	syl2anc 656	. . . . . . . . . . . . . . 15
22		leweon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
23		r0weon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
24	22, 23	r0weon 8169	. . . . . . . . . . . . . . . 16 $/\$ Se
25	24	simpli 455	. . . . . . . . . . . . . . 15
26		wess 4696	. . . . . . . . . . . . . . 15
27	21, 25, 26	mpisyl 18	. . . . . . . . . . . . . 14
28		weinxp 4895	. . . . . . . . . . . . . 14
29	27, 28	sylib 196	. . . . . . . . . . . . 13
30		infxpen.1	. . . . . . . . . . . . . 14
31		weeq1 4697	. . . . . . . . . . . . . 14
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13
33	29, 32	sylibr 212	. . . . . . . . . . . 12
34		infxpen.4	. . . . . . . . . . . . 13 OrdIso
35	34	oiiso 7741	. . . . . . . . . . . 12 $/\$
36	15, 33, 35	sylancr 658	. . . . . . . . . . 11
37		isof1o 6005	. . . . . . . . . . 11
38		f1ocnv 5643	. . . . . . . . . . 11
39		f1of1 5630	. . . . . . . . . . 11
40	36, 37, 38, 39	4syl 21	. . . . . . . . . 10
41		f1f1orn 5642	. . . . . . . . . 10
42	15	f1oen 7320	. . . . . . . . . 10
43	40, 41, 42	3syl 20	. . . . . . . . 9
44		f1ofn 5632	. . . . . . . . . . 11
45	36, 37, 38, 44	4syl 21	. . . . . . . . . 10
46	36	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$
47	37, 38, 39	3syl 20	. . . . . . . . . . . . . . . . . 18
48		cnvimass 5179	. . . . . . . . . . . . . . . . . . 19
49		inss2 3561	. . . . . . . . . . . . . . . . . . . . . 22
50	30, 49	eqsstri 3376	. . . . . . . . . . . . . . . . . . . . 21
51		dmss 5028	. . . . . . . . . . . . . . . . . . . . 21
52	50, 51	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
53		dmxpid 5048	. . . . . . . . . . . . . . . . . . . 20
54	52, 53	sseqtri 3378	. . . . . . . . . . . . . . . . . . 19
55	48, 54	sstri 3355	. . . . . . . . . . . . . . . . . 18
56		f1ores 5645	. . . . . . . . . . . . . . . . . 18 $/\$
57	47, 55, 56	sylancl 657	. . . . . . . . . . . . . . . . 17
58	15, 15	xpex 6499	. . . . . . . . . . . . . . . . . . . . . 22
59	58	inex2 4424	. . . . . . . . . . . . . . . . . . . . 21
60	30, 59	eqeltri 2505	. . . . . . . . . . . . . . . . . . . 20
61	60	cnvex 6516	. . . . . . . . . . . . . . . . . . 19
62		imaexg 6506	. . . . . . . . . . . . . . . . . . 19
63	61, 62	ax-mp 5	. . . . . . . . . . . . . . . . . 18
64	63	f1oen 7320	. . . . . . . . . . . . . . . . 17
65	46, 57, 64	3syl 20	. . . . . . . . . . . . . . . 16 $/\$
66		sseqin2 3559	. . . . . . . . . . . . . . . . . . 19
67	55, 66	mpbi 208	. . . . . . . . . . . . . . . . . 18
68	67	imaeq2i 5157	. . . . . . . . . . . . . . . . 17
69		isocnv 6010	. . . . . . . . . . . . . . . . . . . 20
70	46, 69	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$
71		simpr 458	. . . . . . . . . . . . . . . . . . 19 $/\$
72		isoini 6018	. . . . . . . . . . . . . . . . . . 19 $/\$
73	70, 71, 72	syl2anc 656	. . . . . . . . . . . . . . . . . 18 $/\$
74		fvex 5691	. . . . . . . . . . . . . . . . . . . . 21
75	74	epini 5189	. . . . . . . . . . . . . . . . . . . 20
76	75	ineq2i 3539	. . . . . . . . . . . . . . . . . . 19
77	34	oicl 7733	. . . . . . . . . . . . . . . . . . . . 21
78		f1of 5631	. . . . . . . . . . . . . . . . . . . . . . 23
79	36, 37, 38, 78	4syl 21	. . . . . . . . . . . . . . . . . . . . . 22
80	79	ffvelrnda 5833	. . . . . . . . . . . . . . . . . . . . 21 $/\$
81		ordelss 4724	. . . . . . . . . . . . . . . . . . . . 21 $/\$
82	77, 80, 81	sylancr 658	. . . . . . . . . . . . . . . . . . . 20 $/\$
83		dfss1 3545	. . . . . . . . . . . . . . . . . . . 20
84	82, 83	sylib 196	. . . . . . . . . . . . . . . . . . 19 $/\$
85	76, 84	syl5eq 2479	. . . . . . . . . . . . . . . . . 18 $/\$
86	73, 85	eqtrd 2467	. . . . . . . . . . . . . . . . 17 $/\$
87	68, 86	syl5eqr 2481	. . . . . . . . . . . . . . . 16 $/\$
88	65, 87	breqtrd 4306	. . . . . . . . . . . . . . 15 $/\$
89	88	ensymd 7350	. . . . . . . . . . . . . 14 $/\$
90		infxpen.3	. . . . . . . . . . . . . . . . . . 19
91		fvex 5691	. . . . . . . . . . . . . . . . . . . 20
92		fvex 5691	. . . . . . . . . . . . . . . . . . . 20
93	91, 92	unex 6369	. . . . . . . . . . . . . . . . . . 19
94	90, 93	eqeltri 2505	. . . . . . . . . . . . . . . . . 18
95	94	sucex 6413	. . . . . . . . . . . . . . . . 17
96	95, 95	xpex 6499	. . . . . . . . . . . . . . . 16
97		xpss 4935	. . . . . . . . . . . . . . . . . . . 20
98		simp3 985	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
99		vex 2967	. . . . . . . . . . . . . . . . . . . . . . 23
100		vex 2967	. . . . . . . . . . . . . . . . . . . . . . . 24
101	100	eliniseg 5188	. . . . . . . . . . . . . . . . . . . . . . 23
102	99, 101	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
103	98, 102	sylib 196	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
104	30	breqi 4288	. . . . . . . . . . . . . . . . . . . . . . 23
105		brin 4331	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
106	104, 105	bitri 249	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
107	106	simprbi 461	. . . . . . . . . . . . . . . . . . . . 21
108		brxp 4859	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
109	108	simplbi 457	. . . . . . . . . . . . . . . . . . . . 21
110	103, 107, 109	3syl 20	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
111	97, 110	sseldi 3344	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
112	17	adantr 462	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
113	112	3adant3 1003	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
114		xp1st 6597	. . . . . . . . . . . . . . . . . . . . . 22
115		onelon 4733	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
116	114, 115	sylan2 471	. . . . . . . . . . . . . . . . . . . . 21 $/\$
117	113, 110, 116	syl2anc 656	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
118		eloni 4718	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119		elxp7 6600	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
120	119	simprbi 461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
121		ordunel 6429	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
122	121	3expib 1185	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
123	118, 120, 122	syl2im 38	. . . . . . . . . . . . . . . . . . . . . . . . 25
124	112, 71, 123	sylc 60	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
125	90, 124	syl5eqel 2519	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
126		simprr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
127	13, 126	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
128		simprl 750	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
129	13, 128	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130		iscard 8135	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131		cardlim 8132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
132		sseq2 3368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133		limeq 4720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
134	132, 133	bibi12d 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
135	131, 134	mpbii 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136	130, 135	sylbir 213	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
137	136	biimpa 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
138	17, 127, 129, 137	syl21anc 1212	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	138	adantr 462	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
140		limsuc 6451	. . . . . . . . . . . . . . . . . . . . . . . 24
141	139, 140	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
142	125, 141	mpbid 210	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
143		onelon 4733	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
144	112, 142, 143	syl2anc 656	. . . . . . . . . . . . . . . . . . . . 21 $/\$
145	144	3adant3 1003	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
146		ssun1 3509	. . . . . . . . . . . . . . . . . . . . 21
147	146	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
148	106	simplbi 457	. . . . . . . . . . . . . . . . . . . . 21
149		df-br 4283	. . . . . . . . . . . . . . . . . . . . . . . . . 26
150	23	eleq2i 2499	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$
151		opabid 4586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
152	149, 150, 151	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\/$ $/\$
153	152	simprbi 461	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$ $/\$
154		simpl 454	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
155	154	orim2i 515	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$ $/\$ $\/$
156	153, 155	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
157		fvex 5691	. . . . . . . . . . . . . . . . . . . . . . . . 25
158		fvex 5691	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	157, 158	unex 6369	. . . . . . . . . . . . . . . . . . . . . . . 24
160	159	elsuc 4777	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
161	156, 160	sylibr 212	. . . . . . . . . . . . . . . . . . . . . 22
162		suceq 4773	. . . . . . . . . . . . . . . . . . . . . . 23
163	90, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
164	161, 163	syl6eleqr 2526	. . . . . . . . . . . . . . . . . . . . 21
165	103, 148, 164	3syl 20	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
166		ontr2 4755	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
167	166	imp 429	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
168	117, 145, 147, 165, 167	syl22anc 1214	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
169		xp2nd 6598	. . . . . . . . . . . . . . . . . . . . . 22
170		onelon 4733	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
171	169, 170	sylan2 471	. . . . . . . . . . . . . . . . . . . . 21 $/\$
172	113, 110, 171	syl2anc 656	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
173		ssun2 3510	. . . . . . . . . . . . . . . . . . . . 21
174	173	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
175		ontr2 4755	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
176	175	imp 429	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
177	172, 145, 174, 165, 176	syl22anc 1214	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
178		elxp7 6600	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
179	178	biimpri 206	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
180	111, 168, 177, 179	syl12anc 1211	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
181	180	3expia 1184	. . . . . . . . . . . . . . . . 17 $/\$
182	181	ssrdv 3352	. . . . . . . . . . . . . . . 16 $/\$
183		ssdomg 7345	. . . . . . . . . . . . . . . 16
184	96, 182, 183	mpsyl 63	. . . . . . . . . . . . . . 15 $/\$
185	129	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$
186		nnfi 7493	. . . . . . . . . . . . . . . . . . . 20
187		xpfi 7573	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
188	187	anidms 640	. . . . . . . . . . . . . . . . . . . . 21
189		isfinite 7848	. . . . . . . . . . . . . . . . . . . . 21
190	188, 189	sylib 196	. . . . . . . . . . . . . . . . . . . 20
191	186, 190	syl 16	. . . . . . . . . . . . . . . . . . 19
192		ssdomg 7345	. . . . . . . . . . . . . . . . . . . 20
193	14, 192	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
194		sdomdomtr 7434	. . . . . . . . . . . . . . . . . . 19 $/\$
195	191, 193, 194	syl2an 474	. . . . . . . . . . . . . . . . . 18 $/\$
196	195	expcom 435	. . . . . . . . . . . . . . . . 17
197	185, 196	syl 16	. . . . . . . . . . . . . . . 16 $/\$
198	127	adantr 462	. . . . . . . . . . . . . . . . . 18 $/\$
199		breq1 4285	. . . . . . . . . . . . . . . . . . 19
200	199	rspccv 3061	. . . . . . . . . . . . . . . . . 18
201	198, 142, 200	sylc 60	. . . . . . . . . . . . . . . . 17 $/\$
202		omelon 7842	. . . . . . . . . . . . . . . . . . 19
203		ontri1 4742	. . . . . . . . . . . . . . . . . . 19 $/\$
204	202, 144, 203	sylancr 658	. . . . . . . . . . . . . . . . . 18 $/\$
205		simplr 749	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
206	13, 205	sylbi 195	. . . . . . . . . . . . . . . . . . . 20
207	206	adantr 462	. . . . . . . . . . . . . . . . . . 19 $/\$
208		sseq2 3368	. . . . . . . . . . . . . . . . . . . . 21
209		xpeq12 4848	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
210	209	anidms 640	. . . . . . . . . . . . . . . . . . . . . 22
211		id 22	. . . . . . . . . . . . . . . . . . . . . 22
212	210, 211	breq12d 4295	. . . . . . . . . . . . . . . . . . . . 21
213	208, 212	imbi12d 320	. . . . . . . . . . . . . . . . . . . 20
214	213	rspccv 3061	. . . . . . . . . . . . . . . . . . 19
215	207, 142, 214	sylc 60	. . . . . . . . . . . . . . . . . 18 $/\$
216	204, 215	sylbird 235	. . . . . . . . . . . . . . . . 17 $/\$
217		ensdomtr 7437	. . . . . . . . . . . . . . . . . 18 $/\$
218	217	expcom 435	. . . . . . . . . . . . . . . . 17
219	201, 216, 218	sylsyld 56	. . . . . . . . . . . . . . . 16 $/\$
220	197, 219	pm2.61d 158	. . . . . . . . . . . . . . 15 $/\$
221		domsdomtr 7436	. . . . . . . . . . . . . . 15 $/\$
222	184, 220, 221	syl2anc 656	. . . . . . . . . . . . . 14 $/\$
223		ensdomtr 7437	. . . . . . . . . . . . . 14 $/\$
224	89, 222, 223	syl2anc 656	. . . . . . . . . . . . 13 $/\$
225		ordelon 4732	. . . . . . . . . . . . . . 15 $/\$
226	77, 80, 225	sylancr 658	. . . . . . . . . . . . . 14 $/\$
227		onenon 8109	. . . . . . . . . . . . . . 15
228	112, 227	syl 16	. . . . . . . . . . . . . 14 $/\$
229		cardsdomel 8134	. . . . . . . . . . . . . 14 $/\$
230	226, 228, 229	syl2anc 656	. . . . . . . . . . . . 13 $/\$
231	224, 230	mpbid 210	. . . . . . . . . . . 12 $/\$
232		eleq2 2496	. . . . . . . . . . . . . 14
233	130, 232	sylbir 213	. . . . . . . . . . . . 13 $/\$
234	112, 198, 233	syl2anc 656	. . . . . . . . . . . 12 $/\$
235	231, 234	mpbid 210	. . . . . . . . . . 11 $/\$
236	235	ralrimiva 2791	. . . . . . . . . 10
237		fnfvrnss 5860	. . . . . . . . . . 11 $/\$
238		ssdomg 7345	. . . . . . . . . . 11
239	14, 237, 238	mpsyl 63	. . . . . . . . . 10 $/\$
240	45, 236, 239	syl2anc 656	. . . . . . . . 9
241		endomtr 7357	. . . . . . . . 9 $/\$
242	43, 240, 241	syl2anc 656	. . . . . . . 8
243	13, 242	sylbir 213	. . . . . . 7 $/\$ $/\$ $/\$
244		df1o2 6922	. . . . . . . . . . . 12
245		1onn 7068	. . . . . . . . . . . 12
246	244, 245	eqeltrri 2506	. . . . . . . . . . 11
247		nnsdom 7849	. . . . . . . . . . 11
248		sdomdom 7327	. . . . . . . . . . 11
249	246, 247, 248	mp2b 10	. . . . . . . . . 10
250		domtr 7352	. . . . . . . . . 10 $/\$
251	249, 193, 250	sylancr 658	. . . . . . . . 9
252		0ex 4412	. . . . . . . . . . . 12
253	14, 252	xpsnen 7385	. . . . . . . . . . 11
254	253	ensymi 7349	. . . . . . . . . 10
255	14	xpdom2 7396	. . . . . . . . . 10
256		endomtr 7357	. . . . . . . . . 10 $/\$
257	254, 255, 256	sylancr 658	. . . . . . . . 9
258	251, 257	syl 16	. . . . . . . 8
259	258	ad2antrl 722	. . . . . . 7 $/\$ $/\$ $/\$
260		sbth 7421	. . . . . . 7 $/\$
261	243, 259, 260	syl2anc 656	. . . . . 6 $/\$ $/\$ $/\$
262	261	expr 612	. . . . 5 $/\$ $/\$
263		simplr 749	. . . . . . . 8 $/\$ $/\$ $/\$
264		simpll 748	. . . . . . . . 9 $/\$ $/\$ $/\$
265		simprr 751	. . . . . . . . 9 $/\$ $/\$ $/\$
266		rexnal 2718	. . . . . . . . . 10
267		onelss 4750	. . . . . . . . . . . . 13
268		ssdomg 7345	. . . . . . . . . . . . 13
269	267, 268	syld 44	. . . . . . . . . . . 12
270		bren2 7330	. . . . . . . . . . . . 13 $/\$
271	270	simplbi2 622	. . . . . . . . . . . 12
272	269, 271	syl6 33	. . . . . . . . . . 11
273	272	reximdvai 2818	. . . . . . . . . 10
274	266, 273	syl5bir 218	. . . . . . . . 9
275	264, 265, 274	sylc 60	. . . . . . . 8 $/\$ $/\$ $/\$
276		r19.29 2849	. . . . . . . 8 $/\$ $/\$
277	263, 275, 276	syl2anc 656	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
278		simprl 750	. . . . . . . 8 $/\$ $/\$ $/\$
279		onelon 4733	. . . . . . . . . . . . . . . . 17 $/\$
280		ensym 7348	. . . . . . . . . . . . . . . . . 18
281		domentr 7358	. . . . . . . . . . . . . . . . . 18 $/\$
282	193, 280, 281	syl2an 474	. . . . . . . . . . . . . . . . 17 $/\$
283		domnsym 7427	. . . . . . . . . . . . . . . . . . 19
284		nnsdom 7849	. . . . . . . . . . . . . . . . . . 19
285	283, 284	nsyl 121	. . . . . . . . . . . . . . . . . 18
286		ontri1 4742	. . . . . . . . . . . . . . . . . . 19 $/\$
287	202, 286	mpan 665	. . . . . . . . . . . . . . . . . 18
288	285, 287	syl5ibr 221	. . . . . . . . . . . . . . . . 17
289	279, 282, 288	syl2im 38	. . . . . . . . . . . . . . . 16 $/\$ $/\$
290	289	exp3a 436	. . . . . . . . . . . . . . 15 $/\$
291	290	impcom 430	. . . . . . . . . . . . . 14 $/\$ $/\$
292	291	imim1d 75	. . . . . . . . . . . . 13 $/\$ $/\$
293	292	imp32 433	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
294		entr 7351	. . . . . . . . . . . . . . . 16 $/\$
295	294	ancoms 450	. . . . . . . . . . . . . . 15 $/\$
296		xpen 7464	. . . . . . . . . . . . . . . . . 18 $/\$
297	296	anidms 640	. . . . . . . . . . . . . . . . 17
298		entr 7351	. . . . . . . . . . . . . . . . 17 $/\$
299	297, 298	sylan 468	. . . . . . . . . . . . . . . 16 $/\$
300	280, 299	sylan 468	. . . . . . . . . . . . . . 15 $/\$
301	295, 300	syldan 467	. . . . . . . . . . . . . 14 $/\$
302	301	ex 434	. . . . . . . . . . . . 13
303	302	ad2antll 723	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
304	293, 303	mpd 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
305	304	ex 434	. . . . . . . . . 10 $/\$ $/\$ $/\$
306	305	expr 612	. . . . . . . . 9 $/\$ $/\$
307	306	rexlimdv 2832	. . . . . . . 8 $/\$ $/\$
308	278, 264, 307	syl2anc 656	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
309	277, 308	mpd 15	. . . . . 6 $/\$ $/\$ $/\$
310	309	expr 612	. . . . 5 $/\$ $/\$
311	262, 310	pm2.61d 158	. . . 4 $/\$ $/\$
312	311	exp31 601	. . 3
313	6, 12, 312	tfis3 6459	. 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 960

wceq 1364

wcel 1757

wral 2707

wrex 2708

cvv 2964

cun 3316

cin 3317

wss 3318

c0 3627

csn 3867

cop 3873 class class class wbr 4282

copab 4339

cep 4619 Se wse 4666

wwe 4667

word 4707

con0 4708

wlim 4709

csuc 4710

cxp 4827

ccnv 4828

cdm 4829

crn 4830

cres 4831

cima 4832

wfn 5403

wf 5404

wf1 5405

wf1o 5407

cfv 5408

wiso 5409

com 6467

c1st 6566

c2nd 6567

c1o 6903

cen 7297

cdom 7298

csdm 7299

cfn 7300 OrdIsocoi 7713

ccrd 8095

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1671 ax-6 1709 ax-7 1729 ax-8 1759 ax-9 1761 ax-10 1776 ax-11 1781 ax-12 1793 ax-13 1944 ax-ext 2416 ax-rep 4393 ax-sep 4403 ax-nul 4411 ax-pow 4460 ax-pr 4521 ax-un 6363 ax-inf2 7837

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1702 df-eu 2260 df-mo 2261 df-clab 2422 df-cleq 2428 df-clel 2431 df-nfc 2560 df-ne 2600 df-ral 2712 df-rex 2713 df-reu 2714 df-rmo 2715 df-rab 2716 df-v 2966 df-sbc 3178 df-csb 3279 df-dif 3321 df-un 3323 df-in 3325 df-ss 3332 df-pss 3334 df-nul 3628 df-if 3782 df-pw 3852 df-sn 3868 df-pr 3870 df-tp 3872 df-op 3874 df-uni 4082 df-int 4119 df-iun 4163 df-br 4283 df-opab 4341 df-mpt 4342 df-tr 4376 df-eprel 4621 df-id 4625 df-po 4630 df-so 4631 df-fr 4668 df-se 4669 df-we 4670 df-ord 4711 df-on 4712 df-lim 4713 df-suc 4714 df-xp 4835 df-rel 4836 df-cnv 4837 df-co 4838 df-dm 4839 df-rn 4840 df-res 4841 df-ima 4842 df-iota 5371 df-fun 5410 df-fn 5411 df-f 5412 df-f1 5413 df-fo 5414 df-f1o 5415 df-fv 5416 df-isom 5417 df-riota 6041 df-ov 6085 df-oprab 6086 df-mpt2 6087 df-om 6468 df-1st 6568 df-2nd 6569 df-recs 6820 df-rdg 6854 df-1o 6910 df-oadd 6914 df-er 7091 df-en 7301 df-dom 7302 df-sdom 7303 df-fin 7304 df-oi 7714 df-card 8099

This theorem is referenced by: infxpen 8171

W3C validator