infxpenlem - Metamath Proof Explorer

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

Theorem infxpenlem 8391

Description: Lemma for infxpen 8392. (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 3526	. . . 4
2		xpeq12 5018	. . . . . 6 $/\$
3	2	anidms 645	. . . . 5
4		id 22	. . . . 5
5	3, 4	breq12d 4460	. . . 4
6	1, 5	imbi12d 320	. . 3
7		sseq2 3526	. . . 4
8		xpeq12 5018	. . . . . 6 $/\$
9	8	anidms 645	. . . . 5
10		id 22	. . . . 5
11	9, 10	breq12d 4460	. . . 4
12	7, 11	imbi12d 320	. . 3
13		infxpen.2	. . . . . . . 8 $/\$ $/\$ $/\$
14		vex 3116	. . . . . . . . . . . . 13
15	14, 14	xpex 6588	. . . . . . . . . . . 12
16		simpll 753	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
17	13, 16	sylbi 195	. . . . . . . . . . . . . . . . 17
18		onss 6610	. . . . . . . . . . . . . . . . 17
19	17, 18	syl 16	. . . . . . . . . . . . . . . 16
20		xpss12 5108	. . . . . . . . . . . . . . . 16 $/\$
21	19, 19, 20	syl2anc 661	. . . . . . . . . . . . . . 15
22		leweon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
23		r0weon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
24	22, 23	r0weon 8390	. . . . . . . . . . . . . . . 16 $/\$ Se
25	24	simpli 458	. . . . . . . . . . . . . . 15
26		wess 4866	. . . . . . . . . . . . . . 15
27	21, 25, 26	mpisyl 18	. . . . . . . . . . . . . 14
28		weinxp 5067	. . . . . . . . . . . . . 14
29	27, 28	sylib 196	. . . . . . . . . . . . 13
30		infxpen.1	. . . . . . . . . . . . . 14
31		weeq1 4867	. . . . . . . . . . . . . 14
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13
33	29, 32	sylibr 212	. . . . . . . . . . . 12
34		infxpen.4	. . . . . . . . . . . . 13 OrdIso
35	34	oiiso 7962	. . . . . . . . . . . 12 $/\$
36	15, 33, 35	sylancr 663	. . . . . . . . . . 11
37		isof1o 6209	. . . . . . . . . . 11
38		f1ocnv 5828	. . . . . . . . . . 11
39		f1of1 5815	. . . . . . . . . . 11
40	36, 37, 38, 39	4syl 21	. . . . . . . . . 10
41		f1f1orn 5827	. . . . . . . . . 10
42	15	f1oen 7536	. . . . . . . . . 10
43	40, 41, 42	3syl 20	. . . . . . . . 9
44		f1ofn 5817	. . . . . . . . . . 11
45	36, 37, 38, 44	4syl 21	. . . . . . . . . 10
46	36	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
47	37, 38, 39	3syl 20	. . . . . . . . . . . . . . . . . 18
48		cnvimass 5357	. . . . . . . . . . . . . . . . . . 19
49		inss2 3719	. . . . . . . . . . . . . . . . . . . . . 22
50	30, 49	eqsstri 3534	. . . . . . . . . . . . . . . . . . . . 21
51		dmss 5202	. . . . . . . . . . . . . . . . . . . . 21
52	50, 51	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
53		dmxpid 5222	. . . . . . . . . . . . . . . . . . . 20
54	52, 53	sseqtri 3536	. . . . . . . . . . . . . . . . . . 19
55	48, 54	sstri 3513	. . . . . . . . . . . . . . . . . 18
56		f1ores 5830	. . . . . . . . . . . . . . . . . 18 $/\$
57	47, 55, 56	sylancl 662	. . . . . . . . . . . . . . . . 17
58	15, 15	xpex 6588	. . . . . . . . . . . . . . . . . . . . . 22
59	58	inex2 4589	. . . . . . . . . . . . . . . . . . . . 21
60	30, 59	eqeltri 2551	. . . . . . . . . . . . . . . . . . . 20
61	60	cnvex 6731	. . . . . . . . . . . . . . . . . . 19
62		imaexg 6721	. . . . . . . . . . . . . . . . . . 19
63	61, 62	ax-mp 5	. . . . . . . . . . . . . . . . . 18
64	63	f1oen 7536	. . . . . . . . . . . . . . . . 17
65	46, 57, 64	3syl 20	. . . . . . . . . . . . . . . 16 $/\$
66		sseqin2 3717	. . . . . . . . . . . . . . . . . . 19
67	55, 66	mpbi 208	. . . . . . . . . . . . . . . . . 18
68	67	imaeq2i 5335	. . . . . . . . . . . . . . . . 17
69		isocnv 6214	. . . . . . . . . . . . . . . . . . . 20
70	46, 69	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$
71		simpr 461	. . . . . . . . . . . . . . . . . . 19 $/\$
72		isoini 6222	. . . . . . . . . . . . . . . . . . 19 $/\$
73	70, 71, 72	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$
74		fvex 5876	. . . . . . . . . . . . . . . . . . . . 21
75	74	epini 5367	. . . . . . . . . . . . . . . . . . . 20
76	75	ineq2i 3697	. . . . . . . . . . . . . . . . . . 19
77	34	oicl 7954	. . . . . . . . . . . . . . . . . . . . 21
78		f1of 5816	. . . . . . . . . . . . . . . . . . . . . . 23
79	36, 37, 38, 78	4syl 21	. . . . . . . . . . . . . . . . . . . . . 22
80	79	ffvelrnda 6021	. . . . . . . . . . . . . . . . . . . . 21 $/\$
81		ordelss 4894	. . . . . . . . . . . . . . . . . . . . 21 $/\$
82	77, 80, 81	sylancr 663	. . . . . . . . . . . . . . . . . . . 20 $/\$
83		dfss1 3703	. . . . . . . . . . . . . . . . . . . 20
84	82, 83	sylib 196	. . . . . . . . . . . . . . . . . . 19 $/\$
85	76, 84	syl5eq 2520	. . . . . . . . . . . . . . . . . 18 $/\$
86	73, 85	eqtrd 2508	. . . . . . . . . . . . . . . . 17 $/\$
87	68, 86	syl5eqr 2522	. . . . . . . . . . . . . . . 16 $/\$
88	65, 87	breqtrd 4471	. . . . . . . . . . . . . . 15 $/\$
89	88	ensymd 7566	. . . . . . . . . . . . . 14 $/\$
90		infxpen.3	. . . . . . . . . . . . . . . . . . 19
91		fvex 5876	. . . . . . . . . . . . . . . . . . . 20
92		fvex 5876	. . . . . . . . . . . . . . . . . . . 20
93	91, 92	unex 6582	. . . . . . . . . . . . . . . . . . 19
94	90, 93	eqeltri 2551	. . . . . . . . . . . . . . . . . 18
95	94	sucex 6630	. . . . . . . . . . . . . . . . 17
96	95, 95	xpex 6588	. . . . . . . . . . . . . . . 16
97		xpss 5109	. . . . . . . . . . . . . . . . . . . 20
98		simp3 998	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
99		vex 3116	. . . . . . . . . . . . . . . . . . . . . . 23
100		vex 3116	. . . . . . . . . . . . . . . . . . . . . . . 24
101	100	eliniseg 5366	. . . . . . . . . . . . . . . . . . . . . . 23
102	99, 101	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
103	98, 102	sylib 196	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
104	30	breqi 4453	. . . . . . . . . . . . . . . . . . . . . . 23
105		brin 4496	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
106	104, 105	bitri 249	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
107	106	simprbi 464	. . . . . . . . . . . . . . . . . . . . 21
108		brxp 5030	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
109	108	simplbi 460	. . . . . . . . . . . . . . . . . . . . 21
110	103, 107, 109	3syl 20	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
111	97, 110	sseldi 3502	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
112	17	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
113	112	3adant3 1016	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
114		xp1st 6814	. . . . . . . . . . . . . . . . . . . . . 22
115		onelon 4903	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
116	114, 115	sylan2 474	. . . . . . . . . . . . . . . . . . . . 21 $/\$
117	113, 110, 116	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
118		eloni 4888	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119		elxp7 6817	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
120	119	simprbi 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
121		ordunel 6646	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
122	121	3expib 1199	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
123	118, 120, 122	syl2im 38	. . . . . . . . . . . . . . . . . . . . . . . . 25
124	112, 71, 123	sylc 60	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
125	90, 124	syl5eqel 2559	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
126		simprr 756	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
127	13, 126	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
128		simprl 755	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
129	13, 128	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130		iscard 8356	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131		cardlim 8353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
132		sseq2 3526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133		limeq 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1227	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	138	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
140		limsuc 6668	. . . . . . . . . . . . . . . . . . . . . . . 24
141	139, 140	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
142	125, 141	mpbid 210	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
143		onelon 4903	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
144	112, 142, 143	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$
145	144	3adant3 1016	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
146		ssun1 3667	. . . . . . . . . . . . . . . . . . . . 21
147	146	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
148	106	simplbi 460	. . . . . . . . . . . . . . . . . . . . 21
149		df-br 4448	. . . . . . . . . . . . . . . . . . . . . . . . . 26
150	23	eleq2i 2545	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$
151		opabid 4754	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5876	. . . . . . . . . . . . . . . . . . . . . . . . 25
158		fvex 5876	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	157, 158	unex 6582	. . . . . . . . . . . . . . . . . . . . . . . 24
160	159	elsuc 4947	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
161	156, 160	sylibr 212	. . . . . . . . . . . . . . . . . . . . . 22
162		suceq 4943	. . . . . . . . . . . . . . . . . . . . . . 23
163	90, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
164	161, 163	syl6eleqr 2566	. . . . . . . . . . . . . . . . . . . . 21
165	103, 148, 164	3syl 20	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
166		ontr2 4925	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
167	166	imp 429	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
168	117, 145, 147, 165, 167	syl22anc 1229	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
169		xp2nd 6815	. . . . . . . . . . . . . . . . . . . . . 22
170		onelon 4903	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
171	169, 170	sylan2 474	. . . . . . . . . . . . . . . . . . . . 21 $/\$
172	113, 110, 171	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
173		ssun2 3668	. . . . . . . . . . . . . . . . . . . . 21
174	173	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
175		ontr2 4925	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
176	175	imp 429	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
177	172, 145, 174, 165, 176	syl22anc 1229	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
178		elxp7 6817	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
179	178	biimpri 206	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
180	111, 168, 177, 179	syl12anc 1226	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
181	180	3expia 1198	. . . . . . . . . . . . . . . . 17 $/\$
182	181	ssrdv 3510	. . . . . . . . . . . . . . . 16 $/\$
183		ssdomg 7561	. . . . . . . . . . . . . . . 16
184	96, 182, 183	mpsyl 63	. . . . . . . . . . . . . . 15 $/\$
185	129	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
186		nnfi 7710	. . . . . . . . . . . . . . . . . . . 20
187		xpfi 7791	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
188	187	anidms 645	. . . . . . . . . . . . . . . . . . . . 21
189		isfinite 8069	. . . . . . . . . . . . . . . . . . . . 21
190	188, 189	sylib 196	. . . . . . . . . . . . . . . . . . . 20
191	186, 190	syl 16	. . . . . . . . . . . . . . . . . . 19
192		ssdomg 7561	. . . . . . . . . . . . . . . . . . . 20
193	14, 192	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
194		sdomdomtr 7650	. . . . . . . . . . . . . . . . . . 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 4450	. . . . . . . . . . . . . . . . . . 19
200	199	rspccv 3211	. . . . . . . . . . . . . . . . . 18
201	198, 142, 200	sylc 60	. . . . . . . . . . . . . . . . 17 $/\$
202		omelon 8063	. . . . . . . . . . . . . . . . . . 19
203		ontri1 4912	. . . . . . . . . . . . . . . . . . 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 3526	. . . . . . . . . . . . . . . . . . . . 21
209		xpeq12 5018	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
210	209	anidms 645	. . . . . . . . . . . . . . . . . . . . . 22
211		id 22	. . . . . . . . . . . . . . . . . . . . . 22
212	210, 211	breq12d 4460	. . . . . . . . . . . . . . . . . . . . 21
213	208, 212	imbi12d 320	. . . . . . . . . . . . . . . . . . . 20
214	213	rspccv 3211	. . . . . . . . . . . . . . . . . . 19
215	207, 142, 214	sylc 60	. . . . . . . . . . . . . . . . . 18 $/\$
216	204, 215	sylbird 235	. . . . . . . . . . . . . . . . 17 $/\$
217		ensdomtr 7653	. . . . . . . . . . . . . . . . . 18 $/\$
218	217	expcom 435	. . . . . . . . . . . . . . . . 17
219	201, 216, 218	sylsyld 56	. . . . . . . . . . . . . . . 16 $/\$
220	197, 219	pm2.61d 158	. . . . . . . . . . . . . . 15 $/\$
221		domsdomtr 7652	. . . . . . . . . . . . . . 15 $/\$
222	184, 220, 221	syl2anc 661	. . . . . . . . . . . . . 14 $/\$
223		ensdomtr 7653	. . . . . . . . . . . . . 14 $/\$
224	89, 222, 223	syl2anc 661	. . . . . . . . . . . . 13 $/\$
225		ordelon 4902	. . . . . . . . . . . . . . 15 $/\$
226	77, 80, 225	sylancr 663	. . . . . . . . . . . . . 14 $/\$
227		onenon 8330	. . . . . . . . . . . . . . 15
228	112, 227	syl 16	. . . . . . . . . . . . . 14 $/\$
229		cardsdomel 8355	. . . . . . . . . . . . . 14 $/\$
230	226, 228, 229	syl2anc 661	. . . . . . . . . . . . 13 $/\$
231	224, 230	mpbid 210	. . . . . . . . . . . 12 $/\$
232		eleq2 2540	. . . . . . . . . . . . . 14
233	130, 232	sylbir 213	. . . . . . . . . . . . 13 $/\$
234	112, 198, 233	syl2anc 661	. . . . . . . . . . . 12 $/\$
235	231, 234	mpbid 210	. . . . . . . . . . 11 $/\$
236	235	ralrimiva 2878	. . . . . . . . . 10
237		fnfvrnss 6049	. . . . . . . . . . 11 $/\$
238		ssdomg 7561	. . . . . . . . . . 11
239	14, 237, 238	mpsyl 63	. . . . . . . . . 10 $/\$
240	45, 236, 239	syl2anc 661	. . . . . . . . 9
241		endomtr 7573	. . . . . . . . 9 $/\$
242	43, 240, 241	syl2anc 661	. . . . . . . 8
243	13, 242	sylbir 213	. . . . . . 7 $/\$ $/\$ $/\$
244		df1o2 7142	. . . . . . . . . . . 12
245		1onn 7288	. . . . . . . . . . . 12
246	244, 245	eqeltrri 2552	. . . . . . . . . . 11
247		nnsdom 8070	. . . . . . . . . . 11
248		sdomdom 7543	. . . . . . . . . . 11
249	246, 247, 248	mp2b 10	. . . . . . . . . 10
250		domtr 7568	. . . . . . . . . 10 $/\$
251	249, 193, 250	sylancr 663	. . . . . . . . 9
252		0ex 4577	. . . . . . . . . . . 12
253	14, 252	xpsnen 7601	. . . . . . . . . . 11
254	253	ensymi 7565	. . . . . . . . . 10
255	14	xpdom2 7612	. . . . . . . . . 10
256		endomtr 7573	. . . . . . . . . 10 $/\$
257	254, 255, 256	sylancr 663	. . . . . . . . 9
258	251, 257	syl 16	. . . . . . . 8
259	258	ad2antrl 727	. . . . . . 7 $/\$ $/\$ $/\$
260		sbth 7637	. . . . . . 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 2912	. . . . . . . . . 10
267		onelss 4920	. . . . . . . . . . . . 13
268		ssdomg 7561	. . . . . . . . . . . . 13
269	267, 268	syld 44	. . . . . . . . . . . 12
270		bren2 7546	. . . . . . . . . . . . 13 $/\$
271	270	simplbi2 625	. . . . . . . . . . . 12
272	269, 271	syl6 33	. . . . . . . . . . 11
273	272	reximdvai 2935	. . . . . . . . . 10
274	266, 273	syl5bir 218	. . . . . . . . 9
275	264, 265, 274	sylc 60	. . . . . . . 8 $/\$ $/\$ $/\$
276		r19.29 2997	. . . . . . . 8 $/\$ $/\$
277	263, 275, 276	syl2anc 661	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
278		simprl 755	. . . . . . . 8 $/\$ $/\$ $/\$
279		onelon 4903	. . . . . . . . . . . . . . . . 17 $/\$
280		ensym 7564	. . . . . . . . . . . . . . . . . 18
281		domentr 7574	. . . . . . . . . . . . . . . . . 18 $/\$
282	193, 280, 281	syl2an 477	. . . . . . . . . . . . . . . . 17 $/\$
283		domnsym 7643	. . . . . . . . . . . . . . . . . . 19
284		nnsdom 8070	. . . . . . . . . . . . . . . . . . 19
285	283, 284	nsyl 121	. . . . . . . . . . . . . . . . . 18
286		ontri1 4912	. . . . . . . . . . . . . . . . . . 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 7567	. . . . . . . . . . . . . . . 16 $/\$
295	294	ancoms 453	. . . . . . . . . . . . . . 15 $/\$
296		xpen 7680	. . . . . . . . . . . . . . . . . 18 $/\$
297	296	anidms 645	. . . . . . . . . . . . . . . . 17
298		entr 7567	. . . . . . . . . . . . . . . . 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 2953	. . . . . . . 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 6676	. 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 973

wceq 1379

wcel 1767

wral 2814

wrex 2815

cvv 3113

cun 3474

cin 3475

wss 3476

c0 3785

csn 4027

cop 4033 class class class wbr 4447

copab 4504

cep 4789 Se wse 4836

wwe 4837

word 4877

con0 4878

wlim 4879

csuc 4880

cxp 4997

ccnv 4998

cdm 4999

crn 5000

cres 5001

cima 5002

wfn 5583

wf 5584

wf1 5585

wf1o 5587

cfv 5588

wiso 5589

com 6684

c1st 6782

c2nd 6783

c1o 7123

cen 7513

cdom 7514

csdm 7515

cfn 7516 OrdIsocoi 7934

ccrd 8316

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-inf2 8058

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-isom 5597 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-om 6685 df-1st 6784 df-2nd 6785 df-recs 7042 df-rdg 7076 df-1o 7130 df-oadd 7134 df-er 7311 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-oi 7935 df-card 8320

This theorem is referenced by: infxpen 8392

W3C validator