infxpenlem - Metamath Proof Explorer

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

Theorem infxpenlem 8382

Description: Lemma for infxpen 8383. (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 3511	. . . 4
2		xpeq12 5007	. . . . . 6 $/\$
3	2	anidms 643	. . . . 5
4		id 22	. . . . 5
5	3, 4	breq12d 4452	. . . 4
6	1, 5	imbi12d 318	. . 3
7		sseq2 3511	. . . 4
8		xpeq12 5007	. . . . . 6 $/\$
9	8	anidms 643	. . . . 5
10		id 22	. . . . 5
11	9, 10	breq12d 4452	. . . 4
12	7, 11	imbi12d 318	. . 3
13		infxpen.2	. . . . . . . 8 $/\$ $/\$ $/\$
14		vex 3109	. . . . . . . . . . . . 13
15	14, 14	xpex 6577	. . . . . . . . . . . 12
16		simpll 751	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
17	13, 16	sylbi 195	. . . . . . . . . . . . . . . . 17
18		onss 6599	. . . . . . . . . . . . . . . . 17
19	17, 18	syl 16	. . . . . . . . . . . . . . . 16
20		xpss12 5096	. . . . . . . . . . . . . . . 16 $/\$
21	19, 19, 20	syl2anc 659	. . . . . . . . . . . . . . 15
22		leweon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
23		r0weon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
24	22, 23	r0weon 8381	. . . . . . . . . . . . . . . 16 $/\$ Se
25	24	simpli 456	. . . . . . . . . . . . . . 15
26		wess 4855	. . . . . . . . . . . . . . 15
27	21, 25, 26	mpisyl 18	. . . . . . . . . . . . . 14
28		weinxp 5056	. . . . . . . . . . . . . 14
29	27, 28	sylib 196	. . . . . . . . . . . . 13
30		infxpen.1	. . . . . . . . . . . . . 14
31		weeq1 4856	. . . . . . . . . . . . . 14
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13
33	29, 32	sylibr 212	. . . . . . . . . . . 12
34		infxpen.4	. . . . . . . . . . . . 13 OrdIso
35	34	oiiso 7954	. . . . . . . . . . . 12 $/\$
36	15, 33, 35	sylancr 661	. . . . . . . . . . 11
37		isof1o 6196	. . . . . . . . . . 11
38		f1ocnv 5810	. . . . . . . . . . 11
39		f1of1 5797	. . . . . . . . . . 11
40	36, 37, 38, 39	4syl 21	. . . . . . . . . 10
41		f1f1orn 5809	. . . . . . . . . 10
42	15	f1oen 7529	. . . . . . . . . 10
43	40, 41, 42	3syl 20	. . . . . . . . 9
44		f1ofn 5799	. . . . . . . . . . 11
45	36, 37, 38, 44	4syl 21	. . . . . . . . . 10
46	36	adantr 463	. . . . . . . . . . . . . . . . 17 $/\$
47	37, 38, 39	3syl 20	. . . . . . . . . . . . . . . . . 18
48		cnvimass 5345	. . . . . . . . . . . . . . . . . . 19
49		inss2 3705	. . . . . . . . . . . . . . . . . . . . . 22
50	30, 49	eqsstri 3519	. . . . . . . . . . . . . . . . . . . . 21
51		dmss 5191	. . . . . . . . . . . . . . . . . . . . 21
52	50, 51	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
53		dmxpid 5211	. . . . . . . . . . . . . . . . . . . 20
54	52, 53	sseqtri 3521	. . . . . . . . . . . . . . . . . . 19
55	48, 54	sstri 3498	. . . . . . . . . . . . . . . . . 18
56		f1ores 5812	. . . . . . . . . . . . . . . . . 18 $/\$
57	47, 55, 56	sylancl 660	. . . . . . . . . . . . . . . . 17
58	15, 15	xpex 6577	. . . . . . . . . . . . . . . . . . . . . 22
59	58	inex2 4579	. . . . . . . . . . . . . . . . . . . . 21
60	30, 59	eqeltri 2538	. . . . . . . . . . . . . . . . . . . 20
61	60	cnvex 6720	. . . . . . . . . . . . . . . . . . 19
62		imaexg 6710	. . . . . . . . . . . . . . . . . . 19
63	61, 62	ax-mp 5	. . . . . . . . . . . . . . . . . 18
64	63	f1oen 7529	. . . . . . . . . . . . . . . . 17
65	46, 57, 64	3syl 20	. . . . . . . . . . . . . . . 16 $/\$
66		sseqin2 3703	. . . . . . . . . . . . . . . . . . 19
67	55, 66	mpbi 208	. . . . . . . . . . . . . . . . . 18
68	67	imaeq2i 5323	. . . . . . . . . . . . . . . . 17
69		isocnv 6201	. . . . . . . . . . . . . . . . . . . 20
70	46, 69	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$
71		simpr 459	. . . . . . . . . . . . . . . . . . 19 $/\$
72		isoini 6209	. . . . . . . . . . . . . . . . . . 19 $/\$
73	70, 71, 72	syl2anc 659	. . . . . . . . . . . . . . . . . 18 $/\$
74		fvex 5858	. . . . . . . . . . . . . . . . . . . . 21
75	74	epini 5355	. . . . . . . . . . . . . . . . . . . 20
76	75	ineq2i 3683	. . . . . . . . . . . . . . . . . . 19
77	34	oicl 7946	. . . . . . . . . . . . . . . . . . . . 21
78		f1of 5798	. . . . . . . . . . . . . . . . . . . . . . 23
79	36, 37, 38, 78	4syl 21	. . . . . . . . . . . . . . . . . . . . . 22
80	79	ffvelrnda 6007	. . . . . . . . . . . . . . . . . . . . 21 $/\$
81		ordelss 4883	. . . . . . . . . . . . . . . . . . . . 21 $/\$
82	77, 80, 81	sylancr 661	. . . . . . . . . . . . . . . . . . . 20 $/\$
83		dfss1 3689	. . . . . . . . . . . . . . . . . . . 20
84	82, 83	sylib 196	. . . . . . . . . . . . . . . . . . 19 $/\$
85	76, 84	syl5eq 2507	. . . . . . . . . . . . . . . . . 18 $/\$
86	73, 85	eqtrd 2495	. . . . . . . . . . . . . . . . 17 $/\$
87	68, 86	syl5eqr 2509	. . . . . . . . . . . . . . . 16 $/\$
88	65, 87	breqtrd 4463	. . . . . . . . . . . . . . 15 $/\$
89	88	ensymd 7559	. . . . . . . . . . . . . 14 $/\$
90		infxpen.3	. . . . . . . . . . . . . . . . . . 19
91		fvex 5858	. . . . . . . . . . . . . . . . . . . 20
92		fvex 5858	. . . . . . . . . . . . . . . . . . . 20
93	91, 92	unex 6571	. . . . . . . . . . . . . . . . . . 19
94	90, 93	eqeltri 2538	. . . . . . . . . . . . . . . . . 18
95	94	sucex 6619	. . . . . . . . . . . . . . . . 17
96	95, 95	xpex 6577	. . . . . . . . . . . . . . . 16
97		xpss 5097	. . . . . . . . . . . . . . . . . . . 20
98		simp3 996	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
99		vex 3109	. . . . . . . . . . . . . . . . . . . . . . 23
100		vex 3109	. . . . . . . . . . . . . . . . . . . . . . . 24
101	100	eliniseg 5354	. . . . . . . . . . . . . . . . . . . . . . 23
102	99, 101	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
103	98, 102	sylib 196	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
104	30	breqi 4445	. . . . . . . . . . . . . . . . . . . . . . 23
105		brin 4488	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
106	104, 105	bitri 249	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
107	106	simprbi 462	. . . . . . . . . . . . . . . . . . . . 21
108		brxp 5019	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
109	108	simplbi 458	. . . . . . . . . . . . . . . . . . . . 21
110	103, 107, 109	3syl 20	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
111	97, 110	sseldi 3487	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
112	17	adantr 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
113	112	3adant3 1014	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
114		xp1st 6803	. . . . . . . . . . . . . . . . . . . . . 22
115		onelon 4892	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
116	114, 115	sylan2 472	. . . . . . . . . . . . . . . . . . . . 21 $/\$
117	113, 110, 116	syl2anc 659	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
118		eloni 4877	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119		elxp7 6806	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
120	119	simprbi 462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
121		ordunel 6635	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
122	121	3expib 1197	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
123	118, 120, 122	syl2im 38	. . . . . . . . . . . . . . . . . . . . . . . . 25
124	112, 71, 123	sylc 60	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
125	90, 124	syl5eqel 2546	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
126		simprr 755	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
127	13, 126	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
128		simprl 754	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
129	13, 128	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130		iscard 8347	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131		cardlim 8344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
132		sseq2 3511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133		limeq 4879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
134	132, 133	bibi12d 319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
135	131, 134	mpbii 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136	130, 135	sylbir 213	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
137	136	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
138	17, 127, 129, 137	syl21anc 1225	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	138	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
140		limsuc 6657	. . . . . . . . . . . . . . . . . . . . . . . 24
141	139, 140	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
142	125, 141	mpbid 210	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
143		onelon 4892	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
144	112, 142, 143	syl2anc 659	. . . . . . . . . . . . . . . . . . . . 21 $/\$
145	144	3adant3 1014	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
146		ssun1 3653	. . . . . . . . . . . . . . . . . . . . 21
147	146	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
148	106	simplbi 458	. . . . . . . . . . . . . . . . . . . . 21
149		df-br 4440	. . . . . . . . . . . . . . . . . . . . . . . . . 26
150	23	eleq2i 2532	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$
151		opabid 4743	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
152	149, 150, 151	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\/$ $/\$
153	152	simprbi 462	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$ $/\$
154		simpl 455	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
155	154	orim2i 516	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$ $/\$ $\/$
156	153, 155	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
157		fvex 5858	. . . . . . . . . . . . . . . . . . . . . . . . 25
158		fvex 5858	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	157, 158	unex 6571	. . . . . . . . . . . . . . . . . . . . . . . 24
160	159	elsuc 4936	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
161	156, 160	sylibr 212	. . . . . . . . . . . . . . . . . . . . . 22
162		suceq 4932	. . . . . . . . . . . . . . . . . . . . . . 23
163	90, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
164	161, 163	syl6eleqr 2553	. . . . . . . . . . . . . . . . . . . . 21
165	103, 148, 164	3syl 20	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
166		ontr2 4914	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
167	166	imp 427	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
168	117, 145, 147, 165, 167	syl22anc 1227	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
169		xp2nd 6804	. . . . . . . . . . . . . . . . . . . . . 22
170		onelon 4892	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
171	169, 170	sylan2 472	. . . . . . . . . . . . . . . . . . . . 21 $/\$
172	113, 110, 171	syl2anc 659	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
173		ssun2 3654	. . . . . . . . . . . . . . . . . . . . 21
174	173	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
175		ontr2 4914	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
176	175	imp 427	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
177	172, 145, 174, 165, 176	syl22anc 1227	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
178		elxp7 6806	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
179	178	biimpri 206	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
180	111, 168, 177, 179	syl12anc 1224	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
181	180	3expia 1196	. . . . . . . . . . . . . . . . 17 $/\$
182	181	ssrdv 3495	. . . . . . . . . . . . . . . 16 $/\$
183		ssdomg 7554	. . . . . . . . . . . . . . . 16
184	96, 182, 183	mpsyl 63	. . . . . . . . . . . . . . 15 $/\$
185	129	adantr 463	. . . . . . . . . . . . . . . . 17 $/\$
186		nnfi 7703	. . . . . . . . . . . . . . . . . . . 20
187		xpfi 7783	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
188	187	anidms 643	. . . . . . . . . . . . . . . . . . . . 21
189		isfinite 8060	. . . . . . . . . . . . . . . . . . . . 21
190	188, 189	sylib 196	. . . . . . . . . . . . . . . . . . . 20
191	186, 190	syl 16	. . . . . . . . . . . . . . . . . . 19
192		ssdomg 7554	. . . . . . . . . . . . . . . . . . . 20
193	14, 192	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
194		sdomdomtr 7643	. . . . . . . . . . . . . . . . . . 19 $/\$
195	191, 193, 194	syl2an 475	. . . . . . . . . . . . . . . . . 18 $/\$
196	195	expcom 433	. . . . . . . . . . . . . . . . 17
197	185, 196	syl 16	. . . . . . . . . . . . . . . 16 $/\$
198	127	adantr 463	. . . . . . . . . . . . . . . . . 18 $/\$
199		breq1 4442	. . . . . . . . . . . . . . . . . . 19
200	199	rspccv 3204	. . . . . . . . . . . . . . . . . 18
201	198, 142, 200	sylc 60	. . . . . . . . . . . . . . . . 17 $/\$
202		omelon 8054	. . . . . . . . . . . . . . . . . . 19
203		ontri1 4901	. . . . . . . . . . . . . . . . . . 19 $/\$
204	202, 144, 203	sylancr 661	. . . . . . . . . . . . . . . . . 18 $/\$
205		simplr 753	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
206	13, 205	sylbi 195	. . . . . . . . . . . . . . . . . . . 20
207	206	adantr 463	. . . . . . . . . . . . . . . . . . 19 $/\$
208		sseq2 3511	. . . . . . . . . . . . . . . . . . . . 21
209		xpeq12 5007	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
210	209	anidms 643	. . . . . . . . . . . . . . . . . . . . . 22
211		id 22	. . . . . . . . . . . . . . . . . . . . . 22
212	210, 211	breq12d 4452	. . . . . . . . . . . . . . . . . . . . 21
213	208, 212	imbi12d 318	. . . . . . . . . . . . . . . . . . . 20
214	213	rspccv 3204	. . . . . . . . . . . . . . . . . . 19
215	207, 142, 214	sylc 60	. . . . . . . . . . . . . . . . . 18 $/\$
216	204, 215	sylbird 235	. . . . . . . . . . . . . . . . 17 $/\$
217		ensdomtr 7646	. . . . . . . . . . . . . . . . . 18 $/\$
218	217	expcom 433	. . . . . . . . . . . . . . . . 17
219	201, 216, 218	sylsyld 56	. . . . . . . . . . . . . . . 16 $/\$
220	197, 219	pm2.61d 158	. . . . . . . . . . . . . . 15 $/\$
221		domsdomtr 7645	. . . . . . . . . . . . . . 15 $/\$
222	184, 220, 221	syl2anc 659	. . . . . . . . . . . . . 14 $/\$
223		ensdomtr 7646	. . . . . . . . . . . . . 14 $/\$
224	89, 222, 223	syl2anc 659	. . . . . . . . . . . . 13 $/\$
225		ordelon 4891	. . . . . . . . . . . . . . 15 $/\$
226	77, 80, 225	sylancr 661	. . . . . . . . . . . . . 14 $/\$
227		onenon 8321	. . . . . . . . . . . . . . 15
228	112, 227	syl 16	. . . . . . . . . . . . . 14 $/\$
229		cardsdomel 8346	. . . . . . . . . . . . . 14 $/\$
230	226, 228, 229	syl2anc 659	. . . . . . . . . . . . 13 $/\$
231	224, 230	mpbid 210	. . . . . . . . . . . 12 $/\$
232		eleq2 2527	. . . . . . . . . . . . . 14
233	130, 232	sylbir 213	. . . . . . . . . . . . 13 $/\$
234	112, 198, 233	syl2anc 659	. . . . . . . . . . . 12 $/\$
235	231, 234	mpbid 210	. . . . . . . . . . 11 $/\$
236	235	ralrimiva 2868	. . . . . . . . . 10
237		fnfvrnss 6035	. . . . . . . . . . 11 $/\$
238		ssdomg 7554	. . . . . . . . . . 11
239	14, 237, 238	mpsyl 63	. . . . . . . . . 10 $/\$
240	45, 236, 239	syl2anc 659	. . . . . . . . 9
241		endomtr 7566	. . . . . . . . 9 $/\$
242	43, 240, 241	syl2anc 659	. . . . . . . 8
243	13, 242	sylbir 213	. . . . . . 7 $/\$ $/\$ $/\$
244		df1o2 7134	. . . . . . . . . . . 12
245		1onn 7280	. . . . . . . . . . . 12
246	244, 245	eqeltrri 2539	. . . . . . . . . . 11
247		nnsdom 8061	. . . . . . . . . . 11
248		sdomdom 7536	. . . . . . . . . . 11
249	246, 247, 248	mp2b 10	. . . . . . . . . 10
250		domtr 7561	. . . . . . . . . 10 $/\$
251	249, 193, 250	sylancr 661	. . . . . . . . 9
252		0ex 4569	. . . . . . . . . . . 12
253	14, 252	xpsnen 7594	. . . . . . . . . . 11
254	253	ensymi 7558	. . . . . . . . . 10
255	14	xpdom2 7605	. . . . . . . . . 10
256		endomtr 7566	. . . . . . . . . 10 $/\$
257	254, 255, 256	sylancr 661	. . . . . . . . 9
258	251, 257	syl 16	. . . . . . . 8
259	258	ad2antrl 725	. . . . . . 7 $/\$ $/\$ $/\$
260		sbth 7630	. . . . . . 7 $/\$
261	243, 259, 260	syl2anc 659	. . . . . 6 $/\$ $/\$ $/\$
262	261	expr 613	. . . . 5 $/\$ $/\$
263		simplr 753	. . . . . . . 8 $/\$ $/\$ $/\$
264		simpll 751	. . . . . . . . 9 $/\$ $/\$ $/\$
265		simprr 755	. . . . . . . . 9 $/\$ $/\$ $/\$
266		rexnal 2902	. . . . . . . . . 10
267		onelss 4909	. . . . . . . . . . . . 13
268		ssdomg 7554	. . . . . . . . . . . . 13
269	267, 268	syld 44	. . . . . . . . . . . 12
270		bren2 7539	. . . . . . . . . . . . 13 $/\$
271	270	simplbi2 623	. . . . . . . . . . . 12
272	269, 271	syl6 33	. . . . . . . . . . 11
273	272	reximdvai 2926	. . . . . . . . . 10
274	266, 273	syl5bir 218	. . . . . . . . 9
275	264, 265, 274	sylc 60	. . . . . . . 8 $/\$ $/\$ $/\$
276		r19.29 2989	. . . . . . . 8 $/\$ $/\$
277	263, 275, 276	syl2anc 659	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
278		simprl 754	. . . . . . . 8 $/\$ $/\$ $/\$
279		onelon 4892	. . . . . . . . . . . . . . . . 17 $/\$
280		ensym 7557	. . . . . . . . . . . . . . . . . 18
281		domentr 7567	. . . . . . . . . . . . . . . . . 18 $/\$
282	193, 280, 281	syl2an 475	. . . . . . . . . . . . . . . . 17 $/\$
283		domnsym 7636	. . . . . . . . . . . . . . . . . . 19
284		nnsdom 8061	. . . . . . . . . . . . . . . . . . 19
285	283, 284	nsyl 121	. . . . . . . . . . . . . . . . . 18
286		ontri1 4901	. . . . . . . . . . . . . . . . . . 19 $/\$
287	202, 286	mpan 668	. . . . . . . . . . . . . . . . . 18
288	285, 287	syl5ibr 221	. . . . . . . . . . . . . . . . 17
289	279, 282, 288	syl2im 38	. . . . . . . . . . . . . . . 16 $/\$ $/\$
290	289	expd 434	. . . . . . . . . . . . . . 15 $/\$
291	290	impcom 428	. . . . . . . . . . . . . 14 $/\$ $/\$
292	291	imim1d 75	. . . . . . . . . . . . 13 $/\$ $/\$
293	292	imp32 431	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
294		entr 7560	. . . . . . . . . . . . . . . 16 $/\$
295	294	ancoms 451	. . . . . . . . . . . . . . 15 $/\$
296		xpen 7673	. . . . . . . . . . . . . . . . . 18 $/\$
297	296	anidms 643	. . . . . . . . . . . . . . . . 17
298		entr 7560	. . . . . . . . . . . . . . . . 17 $/\$
299	297, 298	sylan 469	. . . . . . . . . . . . . . . 16 $/\$
300	280, 299	sylan 469	. . . . . . . . . . . . . . 15 $/\$
301	295, 300	syldan 468	. . . . . . . . . . . . . 14 $/\$
302	301	ex 432	. . . . . . . . . . . . 13
303	302	ad2antll 726	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
304	293, 303	mpd 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
305	304	ex 432	. . . . . . . . . 10 $/\$ $/\$ $/\$
306	305	expr 613	. . . . . . . . 9 $/\$ $/\$
307	306	rexlimdv 2944	. . . . . . . 8 $/\$ $/\$
308	278, 264, 307	syl2anc 659	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
309	277, 308	mpd 15	. . . . . 6 $/\$ $/\$ $/\$
310	309	expr 613	. . . . 5 $/\$ $/\$
311	262, 310	pm2.61d 158	. . . 4 $/\$ $/\$
312	311	exp31 602	. . 3
313	6, 12, 312	tfis3 6665	. 2
314	313	imp 427	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367 $/\$ w3a 971

wceq 1398

wcel 1823

wral 2804

wrex 2805

cvv 3106

cun 3459

cin 3460

wss 3461

c0 3783

csn 4016

cop 4022 class class class wbr 4439

copab 4496

cep 4778 Se wse 4825

wwe 4826

word 4866

con0 4867

wlim 4868

csuc 4869

cxp 4986

ccnv 4987

cdm 4988

crn 4989

cres 4990

cima 4991

wfn 5565

wf 5566

wf1 5567

wf1o 5569

cfv 5570

wiso 5571

com 6673

c1st 6771

c2nd 6772

c1o 7115

cen 7506

cdom 7507

csdm 7508

cfn 7509 OrdIsocoi 7926

ccrd 8307

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-rep 4550 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565 ax-inf2 8049

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-ral 2809 df-rex 2810 df-reu 2811 df-rmo 2812 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-tp 4021 df-op 4023 df-uni 4236 df-int 4272 df-iun 4317 df-br 4440 df-opab 4498 df-mpt 4499 df-tr 4533 df-eprel 4780 df-id 4784 df-po 4789 df-so 4790 df-fr 4827 df-se 4828 df-we 4829 df-ord 4870 df-on 4871 df-lim 4872 df-suc 4873 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-isom 5579 df-riota 6232 df-ov 6273 df-oprab 6274 df-mpt2 6275 df-om 6674 df-1st 6773 df-2nd 6774 df-recs 7034 df-rdg 7068 df-1o 7122 df-oadd 7126 df-er 7303 df-en 7510 df-dom 7511 df-sdom 7512 df-fin 7513 df-oi 7927 df-card 8311

This theorem is referenced by: infxpen 8383

W3C validator