infxpenlem - Metamath Proof Explorer

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

Theorem infxpenlem 8462

Description: Lemma for infxpen 8463. (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 3440	. . . 4
2		xpeq12 4858	. . . . . 6 $/\$
3	2	anidms 657	. . . . 5
4		id 22	. . . . 5
5	3, 4	breq12d 4408	. . . 4
6	1, 5	imbi12d 327	. . 3
7		sseq2 3440	. . . 4
8		xpeq12 4858	. . . . . 6 $/\$
9	8	anidms 657	. . . . 5
10		id 22	. . . . 5
11	9, 10	breq12d 4408	. . . 4
12	7, 11	imbi12d 327	. . 3
13		infxpen.2	. . . . . . . 8 $/\$ $/\$ $/\$
14		vex 3034	. . . . . . . . . . . . 13
15	14, 14	xpex 6614	. . . . . . . . . . . 12
16		simpll 768	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
17	13, 16	sylbi 200	. . . . . . . . . . . . . . . . 17
18		onss 6636	. . . . . . . . . . . . . . . . 17
19	17, 18	syl 17	. . . . . . . . . . . . . . . 16
20		xpss12 4945	. . . . . . . . . . . . . . . 16 $/\$
21	19, 19, 20	syl2anc 673	. . . . . . . . . . . . . . 15
22		leweon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
23		r0weon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
24	22, 23	r0weon 8461	. . . . . . . . . . . . . . . 16 $/\$ Se
25	24	simpli 465	. . . . . . . . . . . . . . 15
26		wess 4826	. . . . . . . . . . . . . . 15
27	21, 25, 26	mpisyl 21	. . . . . . . . . . . . . 14
28		weinxp 4907	. . . . . . . . . . . . . 14
29	27, 28	sylib 201	. . . . . . . . . . . . 13
30		infxpen.1	. . . . . . . . . . . . . 14
31		weeq1 4827	. . . . . . . . . . . . . 14
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13
33	29, 32	sylibr 217	. . . . . . . . . . . 12
34		infxpen.4	. . . . . . . . . . . . 13 OrdIso
35	34	oiiso 8070	. . . . . . . . . . . 12 $/\$
36	15, 33, 35	sylancr 676	. . . . . . . . . . 11
37		isof1o 6234	. . . . . . . . . . 11
38		f1ocnv 5840	. . . . . . . . . . 11
39		f1of1 5827	. . . . . . . . . . 11
40	36, 37, 38, 39	4syl 19	. . . . . . . . . 10
41		f1f1orn 5839	. . . . . . . . . 10
42	15	f1oen 7608	. . . . . . . . . 10
43	40, 41, 42	3syl 18	. . . . . . . . 9
44		f1ofn 5829	. . . . . . . . . . 11
45	36, 37, 38, 44	4syl 19	. . . . . . . . . 10
46	36	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$
47	37, 38, 39	3syl 18	. . . . . . . . . . . . . . . . . 18
48		cnvimass 5194	. . . . . . . . . . . . . . . . . . 19
49		inss2 3644	. . . . . . . . . . . . . . . . . . . . . 22
50	30, 49	eqsstri 3448	. . . . . . . . . . . . . . . . . . . . 21
51		dmss 5039	. . . . . . . . . . . . . . . . . . . . 21
52	50, 51	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
53		dmxpid 5060	. . . . . . . . . . . . . . . . . . . 20
54	52, 53	sseqtri 3450	. . . . . . . . . . . . . . . . . . 19
55	48, 54	sstri 3427	. . . . . . . . . . . . . . . . . 18
56		f1ores 5842	. . . . . . . . . . . . . . . . . 18 $/\$
57	47, 55, 56	sylancl 675	. . . . . . . . . . . . . . . . 17
58	15, 15	xpex 6614	. . . . . . . . . . . . . . . . . . . . . 22
59	58	inex2 4538	. . . . . . . . . . . . . . . . . . . . 21
60	30, 59	eqeltri 2545	. . . . . . . . . . . . . . . . . . . 20
61	60	cnvex 6759	. . . . . . . . . . . . . . . . . . 19
62		imaexg 6749	. . . . . . . . . . . . . . . . . . 19
63	61, 62	ax-mp 5	. . . . . . . . . . . . . . . . . 18
64	63	f1oen 7608	. . . . . . . . . . . . . . . . 17
65	46, 57, 64	3syl 18	. . . . . . . . . . . . . . . 16 $/\$
66		sseqin2 3642	. . . . . . . . . . . . . . . . . . 19
67	55, 66	mpbi 213	. . . . . . . . . . . . . . . . . 18
68	67	imaeq2i 5172	. . . . . . . . . . . . . . . . 17
69		isocnv 6239	. . . . . . . . . . . . . . . . . . . 20
70	46, 69	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$
71		simpr 468	. . . . . . . . . . . . . . . . . . 19 $/\$
72		isoini 6247	. . . . . . . . . . . . . . . . . . 19 $/\$
73	70, 71, 72	syl2anc 673	. . . . . . . . . . . . . . . . . 18 $/\$
74		fvex 5889	. . . . . . . . . . . . . . . . . . . . 21
75	74	epini 5204	. . . . . . . . . . . . . . . . . . . 20
76	75	ineq2i 3622	. . . . . . . . . . . . . . . . . . 19
77	34	oicl 8062	. . . . . . . . . . . . . . . . . . . . 21
78		f1of 5828	. . . . . . . . . . . . . . . . . . . . . . 23
79	36, 37, 38, 78	4syl 19	. . . . . . . . . . . . . . . . . . . . . 22
80	79	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . 21 $/\$
81		ordelss 5446	. . . . . . . . . . . . . . . . . . . . 21 $/\$
82	77, 80, 81	sylancr 676	. . . . . . . . . . . . . . . . . . . 20 $/\$
83		dfss1 3628	. . . . . . . . . . . . . . . . . . . 20
84	82, 83	sylib 201	. . . . . . . . . . . . . . . . . . 19 $/\$
85	76, 84	syl5eq 2517	. . . . . . . . . . . . . . . . . 18 $/\$
86	73, 85	eqtrd 2505	. . . . . . . . . . . . . . . . 17 $/\$
87	68, 86	syl5eqr 2519	. . . . . . . . . . . . . . . 16 $/\$
88	65, 87	breqtrd 4420	. . . . . . . . . . . . . . 15 $/\$
89	88	ensymd 7638	. . . . . . . . . . . . . 14 $/\$
90		infxpen.3	. . . . . . . . . . . . . . . . . . 19
91		fvex 5889	. . . . . . . . . . . . . . . . . . . 20
92		fvex 5889	. . . . . . . . . . . . . . . . . . . 20
93	91, 92	unex 6608	. . . . . . . . . . . . . . . . . . 19
94	90, 93	eqeltri 2545	. . . . . . . . . . . . . . . . . 18
95	94	sucex 6657	. . . . . . . . . . . . . . . . 17
96	95, 95	xpex 6614	. . . . . . . . . . . . . . . 16
97		xpss 4946	. . . . . . . . . . . . . . . . . . . 20
98		simp3 1032	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
99		vex 3034	. . . . . . . . . . . . . . . . . . . . . . 23
100		vex 3034	. . . . . . . . . . . . . . . . . . . . . . . 24
101	100	eliniseg 5203	. . . . . . . . . . . . . . . . . . . . . . 23
102	99, 101	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
103	98, 102	sylib 201	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
104	30	breqi 4401	. . . . . . . . . . . . . . . . . . . . . . 23
105		brin 4445	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
106	104, 105	bitri 257	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
107	106	simprbi 471	. . . . . . . . . . . . . . . . . . . . 21
108		brxp 4870	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
109	108	simplbi 467	. . . . . . . . . . . . . . . . . . . . 21
110	103, 107, 109	3syl 18	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
111	97, 110	sseldi 3416	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
112	17	adantr 472	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
113	112	3adant3 1050	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
114		xp1st 6842	. . . . . . . . . . . . . . . . . . . . . 22
115		onelon 5455	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
116	114, 115	sylan2 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
117	113, 110, 116	syl2anc 673	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
118		eloni 5440	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119		elxp7 6845	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
120	119	simprbi 471	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
121		ordunel 6673	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
122	121	3expib 1234	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
123	118, 120, 122	syl2im 38	. . . . . . . . . . . . . . . . . . . . . . . . 25
124	112, 71, 123	sylc 61	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
125	90, 124	syl5eqel 2553	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
126		simprr 774	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
127	13, 126	sylbi 200	. . . . . . . . . . . . . . . . . . . . . . . . . 26
128		simprl 772	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
129	13, 128	sylbi 200	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130		iscard 8427	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131		cardlim 8424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
132		sseq2 3440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133		limeq 5442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
134	132, 133	bibi12d 328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
135	131, 134	mpbii 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136	130, 135	sylbir 218	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
137	136	biimpa 492	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
138	17, 127, 129, 137	syl21anc 1291	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	138	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
140		limsuc 6695	. . . . . . . . . . . . . . . . . . . . . . . 24
141	139, 140	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
142	125, 141	mpbid 215	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
143		onelon 5455	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
144	112, 142, 143	syl2anc 673	. . . . . . . . . . . . . . . . . . . . 21 $/\$
145	144	3adant3 1050	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
146		ssun1 3588	. . . . . . . . . . . . . . . . . . . . 21
147	146	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
148	106	simplbi 467	. . . . . . . . . . . . . . . . . . . . 21
149		df-br 4396	. . . . . . . . . . . . . . . . . . . . . . . . . 26
150	23	eleq2i 2541	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$
151		opabid 4708	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
152	149, 150, 151	3bitri 279	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\/$ $/\$
153	152	simprbi 471	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$ $/\$
154		simpl 464	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
155	154	orim2i 527	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$ $/\$ $\/$
156	153, 155	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
157		fvex 5889	. . . . . . . . . . . . . . . . . . . . . . . . 25
158		fvex 5889	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	157, 158	unex 6608	. . . . . . . . . . . . . . . . . . . . . . . 24
160	159	elsuc 5499	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
161	156, 160	sylibr 217	. . . . . . . . . . . . . . . . . . . . . 22
162		suceq 5495	. . . . . . . . . . . . . . . . . . . . . . 23
163	90, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
164	161, 163	syl6eleqr 2560	. . . . . . . . . . . . . . . . . . . . 21
165	103, 148, 164	3syl 18	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
166		ontr2 5477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
167	166	imp 436	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
168	117, 145, 147, 165, 167	syl22anc 1293	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
169		xp2nd 6843	. . . . . . . . . . . . . . . . . . . . . 22
170		onelon 5455	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
171	169, 170	sylan2 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
172	113, 110, 171	syl2anc 673	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
173		ssun2 3589	. . . . . . . . . . . . . . . . . . . . 21
174	173	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
175		ontr2 5477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
176	175	imp 436	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
177	172, 145, 174, 165, 176	syl22anc 1293	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
178		elxp7 6845	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
179	178	biimpri 211	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
180	111, 168, 177, 179	syl12anc 1290	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
181	180	3expia 1233	. . . . . . . . . . . . . . . . 17 $/\$
182	181	ssrdv 3424	. . . . . . . . . . . . . . . 16 $/\$
183		ssdomg 7633	. . . . . . . . . . . . . . . 16
184	96, 182, 183	mpsyl 64	. . . . . . . . . . . . . . 15 $/\$
185	129	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$
186		nnfi 7783	. . . . . . . . . . . . . . . . . . . 20
187		xpfi 7860	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
188	187	anidms 657	. . . . . . . . . . . . . . . . . . . . 21
189		isfinite 8175	. . . . . . . . . . . . . . . . . . . . 21
190	188, 189	sylib 201	. . . . . . . . . . . . . . . . . . . 20
191	186, 190	syl 17	. . . . . . . . . . . . . . . . . . 19
192		ssdomg 7633	. . . . . . . . . . . . . . . . . . . 20
193	14, 192	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
194		sdomdomtr 7723	. . . . . . . . . . . . . . . . . . 19 $/\$
195	191, 193, 194	syl2an 485	. . . . . . . . . . . . . . . . . 18 $/\$
196	195	expcom 442	. . . . . . . . . . . . . . . . 17
197	185, 196	syl 17	. . . . . . . . . . . . . . . 16 $/\$
198	127	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$
199		breq1 4398	. . . . . . . . . . . . . . . . . . 19
200	199	rspccv 3133	. . . . . . . . . . . . . . . . . 18
201	198, 142, 200	sylc 61	. . . . . . . . . . . . . . . . 17 $/\$
202		omelon 8169	. . . . . . . . . . . . . . . . . . 19
203		ontri1 5464	. . . . . . . . . . . . . . . . . . 19 $/\$
204	202, 144, 203	sylancr 676	. . . . . . . . . . . . . . . . . 18 $/\$
205		simplr 770	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
206	13, 205	sylbi 200	. . . . . . . . . . . . . . . . . . . 20
207	206	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$
208		sseq2 3440	. . . . . . . . . . . . . . . . . . . . 21
209		xpeq12 4858	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
210	209	anidms 657	. . . . . . . . . . . . . . . . . . . . . 22
211		id 22	. . . . . . . . . . . . . . . . . . . . . 22
212	210, 211	breq12d 4408	. . . . . . . . . . . . . . . . . . . . 21
213	208, 212	imbi12d 327	. . . . . . . . . . . . . . . . . . . 20
214	213	rspccv 3133	. . . . . . . . . . . . . . . . . . 19
215	207, 142, 214	sylc 61	. . . . . . . . . . . . . . . . . 18 $/\$
216	204, 215	sylbird 243	. . . . . . . . . . . . . . . . 17 $/\$
217		ensdomtr 7726	. . . . . . . . . . . . . . . . . 18 $/\$
218	217	expcom 442	. . . . . . . . . . . . . . . . 17
219	201, 216, 218	sylsyld 57	. . . . . . . . . . . . . . . 16 $/\$
220	197, 219	pm2.61d 163	. . . . . . . . . . . . . . 15 $/\$
221		domsdomtr 7725	. . . . . . . . . . . . . . 15 $/\$
222	184, 220, 221	syl2anc 673	. . . . . . . . . . . . . 14 $/\$
223		ensdomtr 7726	. . . . . . . . . . . . . 14 $/\$
224	89, 222, 223	syl2anc 673	. . . . . . . . . . . . 13 $/\$
225		ordelon 5454	. . . . . . . . . . . . . . 15 $/\$
226	77, 80, 225	sylancr 676	. . . . . . . . . . . . . 14 $/\$
227		onenon 8401	. . . . . . . . . . . . . . 15
228	112, 227	syl 17	. . . . . . . . . . . . . 14 $/\$
229		cardsdomel 8426	. . . . . . . . . . . . . 14 $/\$
230	226, 228, 229	syl2anc 673	. . . . . . . . . . . . 13 $/\$
231	224, 230	mpbid 215	. . . . . . . . . . . 12 $/\$
232		eleq2 2538	. . . . . . . . . . . . . 14
233	130, 232	sylbir 218	. . . . . . . . . . . . 13 $/\$
234	112, 198, 233	syl2anc 673	. . . . . . . . . . . 12 $/\$
235	231, 234	mpbid 215	. . . . . . . . . . 11 $/\$
236	235	ralrimiva 2809	. . . . . . . . . 10
237		fnfvrnss 6066	. . . . . . . . . . 11 $/\$
238		ssdomg 7633	. . . . . . . . . . 11
239	14, 237, 238	mpsyl 64	. . . . . . . . . 10 $/\$
240	45, 236, 239	syl2anc 673	. . . . . . . . 9
241		endomtr 7645	. . . . . . . . 9 $/\$
242	43, 240, 241	syl2anc 673	. . . . . . . 8
243	13, 242	sylbir 218	. . . . . . 7 $/\$ $/\$ $/\$
244		df1o2 7212	. . . . . . . . . . . 12
245		1onn 7358	. . . . . . . . . . . 12
246	244, 245	eqeltrri 2546	. . . . . . . . . . 11
247		nnsdom 8177	. . . . . . . . . . 11
248		sdomdom 7615	. . . . . . . . . . 11
249	246, 247, 248	mp2b 10	. . . . . . . . . 10
250		domtr 7640	. . . . . . . . . 10 $/\$
251	249, 193, 250	sylancr 676	. . . . . . . . 9
252		0ex 4528	. . . . . . . . . . . 12
253	14, 252	xpsnen 7674	. . . . . . . . . . 11
254	253	ensymi 7637	. . . . . . . . . 10
255	14	xpdom2 7685	. . . . . . . . . 10
256		endomtr 7645	. . . . . . . . . 10 $/\$
257	254, 255, 256	sylancr 676	. . . . . . . . 9
258	251, 257	syl 17	. . . . . . . 8
259	258	ad2antrl 742	. . . . . . 7 $/\$ $/\$ $/\$
260		sbth 7710	. . . . . . 7 $/\$
261	243, 259, 260	syl2anc 673	. . . . . 6 $/\$ $/\$ $/\$
262	261	expr 626	. . . . 5 $/\$ $/\$
263		simplr 770	. . . . . . . 8 $/\$ $/\$ $/\$
264		simpll 768	. . . . . . . . 9 $/\$ $/\$ $/\$
265		simprr 774	. . . . . . . . 9 $/\$ $/\$ $/\$
266		rexnal 2836	. . . . . . . . . 10
267		onelss 5472	. . . . . . . . . . . . 13
268		ssdomg 7633	. . . . . . . . . . . . 13
269	267, 268	syld 44	. . . . . . . . . . . 12
270		bren2 7618	. . . . . . . . . . . . 13 $/\$
271	270	simplbi2 637	. . . . . . . . . . . 12
272	269, 271	syl6 33	. . . . . . . . . . 11
273	272	reximdvai 2856	. . . . . . . . . 10
274	266, 273	syl5bir 226	. . . . . . . . 9
275	264, 265, 274	sylc 61	. . . . . . . 8 $/\$ $/\$ $/\$
276		r19.29 2912	. . . . . . . 8 $/\$ $/\$
277	263, 275, 276	syl2anc 673	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
278		simprl 772	. . . . . . . 8 $/\$ $/\$ $/\$
279		onelon 5455	. . . . . . . . . . . . . . . . 17 $/\$
280		ensym 7636	. . . . . . . . . . . . . . . . . 18
281		domentr 7646	. . . . . . . . . . . . . . . . . 18 $/\$
282	193, 280, 281	syl2an 485	. . . . . . . . . . . . . . . . 17 $/\$
283		domnsym 7716	. . . . . . . . . . . . . . . . . . 19
284		nnsdom 8177	. . . . . . . . . . . . . . . . . . 19
285	283, 284	nsyl 125	. . . . . . . . . . . . . . . . . 18
286		ontri1 5464	. . . . . . . . . . . . . . . . . . 19 $/\$
287	202, 286	mpan 684	. . . . . . . . . . . . . . . . . 18
288	285, 287	syl5ibr 229	. . . . . . . . . . . . . . . . 17
289	279, 282, 288	syl2im 38	. . . . . . . . . . . . . . . 16 $/\$ $/\$
290	289	expd 443	. . . . . . . . . . . . . . 15 $/\$
291	290	impcom 437	. . . . . . . . . . . . . 14 $/\$ $/\$
292	291	imim1d 77	. . . . . . . . . . . . 13 $/\$ $/\$
293	292	imp32 440	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
294		entr 7639	. . . . . . . . . . . . . . . 16 $/\$
295	294	ancoms 460	. . . . . . . . . . . . . . 15 $/\$
296		xpen 7753	. . . . . . . . . . . . . . . . . 18 $/\$
297	296	anidms 657	. . . . . . . . . . . . . . . . 17
298		entr 7639	. . . . . . . . . . . . . . . . 17 $/\$
299	297, 298	sylan 479	. . . . . . . . . . . . . . . 16 $/\$
300	280, 299	sylan 479	. . . . . . . . . . . . . . 15 $/\$
301	295, 300	syldan 478	. . . . . . . . . . . . . 14 $/\$
302	301	ex 441	. . . . . . . . . . . . 13
303	302	ad2antll 743	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
304	293, 303	mpd 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
305	304	ex 441	. . . . . . . . . 10 $/\$ $/\$ $/\$
306	305	expr 626	. . . . . . . . 9 $/\$ $/\$
307	306	rexlimdv 2870	. . . . . . . 8 $/\$ $/\$
308	278, 264, 307	syl2anc 673	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
309	277, 308	mpd 15	. . . . . 6 $/\$ $/\$ $/\$
310	309	expr 626	. . . . 5 $/\$ $/\$
311	262, 310	pm2.61d 163	. . . 4 $/\$ $/\$
312	311	exp31 615	. . 3
313	6, 12, 312	tfis3 6703	. 2
314	313	imp 436	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

wral 2756

wrex 2757

cvv 3031

cun 3388

cin 3389

wss 3390

c0 3722

csn 3959

cop 3965 class class class wbr 4395

copab 4453

cep 4748 Se wse 4796

wwe 4797

cxp 4837

ccnv 4838

cdm 4839

crn 4840

cres 4841

cima 4842

word 5429

con0 5430

wlim 5431

csuc 5432

wfn 5584

wf 5585

wf1 5586

wf1o 5588

cfv 5589

wiso 5590

com 6711

c1st 6810

c2nd 6811

c1o 7193

cen 7584

cdom 7585

csdm 7586

cfn 7587 OrdIsocoi 8042

ccrd 8387

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-oadd 7204 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-oi 8043 df-card 8391

This theorem is referenced by: infxpen 8463

W3C validator