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 8444

Description: Lemma for infxpen 8445. (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 3454	. . . 4
2		xpeq12 4853	. . . . . 6 $/\$
3	2	anidms 651	. . . . 5
4		id 22	. . . . 5
5	3, 4	breq12d 4415	. . . 4
6	1, 5	imbi12d 322	. . 3
7		sseq2 3454	. . . 4
8		xpeq12 4853	. . . . . 6 $/\$
9	8	anidms 651	. . . . 5
10		id 22	. . . . 5
11	9, 10	breq12d 4415	. . . 4
12	7, 11	imbi12d 322	. . 3
13		infxpen.2	. . . . . . . 8 $/\$ $/\$ $/\$
14		vex 3048	. . . . . . . . . . . . 13
15	14, 14	xpex 6595	. . . . . . . . . . . 12
16		simpll 760	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
17	13, 16	sylbi 199	. . . . . . . . . . . . . . . . 17
18		onss 6617	. . . . . . . . . . . . . . . . 17
19	17, 18	syl 17	. . . . . . . . . . . . . . . 16
20		xpss12 4940	. . . . . . . . . . . . . . . 16 $/\$
21	19, 19, 20	syl2anc 667	. . . . . . . . . . . . . . 15
22		leweon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
23		r0weon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
24	22, 23	r0weon 8443	. . . . . . . . . . . . . . . 16 $/\$ Se
25	24	simpli 460	. . . . . . . . . . . . . . 15
26		wess 4821	. . . . . . . . . . . . . . 15
27	21, 25, 26	mpisyl 21	. . . . . . . . . . . . . 14
28		weinxp 4902	. . . . . . . . . . . . . 14
29	27, 28	sylib 200	. . . . . . . . . . . . 13
30		infxpen.1	. . . . . . . . . . . . . 14
31		weeq1 4822	. . . . . . . . . . . . . 14
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13
33	29, 32	sylibr 216	. . . . . . . . . . . 12
34		infxpen.4	. . . . . . . . . . . . 13 OrdIso
35	34	oiiso 8052	. . . . . . . . . . . 12 $/\$
36	15, 33, 35	sylancr 669	. . . . . . . . . . 11
37		isof1o 6216	. . . . . . . . . . 11
38		f1ocnv 5826	. . . . . . . . . . 11
39		f1of1 5813	. . . . . . . . . . 11
40	36, 37, 38, 39	4syl 19	. . . . . . . . . 10
41		f1f1orn 5825	. . . . . . . . . 10
42	15	f1oen 7590	. . . . . . . . . 10
43	40, 41, 42	3syl 18	. . . . . . . . 9
44		f1ofn 5815	. . . . . . . . . . 11
45	36, 37, 38, 44	4syl 19	. . . . . . . . . 10
46	36	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
47	37, 38, 39	3syl 18	. . . . . . . . . . . . . . . . . 18
48		cnvimass 5188	. . . . . . . . . . . . . . . . . . 19
49		inss2 3653	. . . . . . . . . . . . . . . . . . . . . 22
50	30, 49	eqsstri 3462	. . . . . . . . . . . . . . . . . . . . 21
51		dmss 5034	. . . . . . . . . . . . . . . . . . . . 21
52	50, 51	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
53		dmxpid 5054	. . . . . . . . . . . . . . . . . . . 20
54	52, 53	sseqtri 3464	. . . . . . . . . . . . . . . . . . 19
55	48, 54	sstri 3441	. . . . . . . . . . . . . . . . . 18
56		f1ores 5828	. . . . . . . . . . . . . . . . . 18 $/\$
57	47, 55, 56	sylancl 668	. . . . . . . . . . . . . . . . 17
58	15, 15	xpex 6595	. . . . . . . . . . . . . . . . . . . . . 22
59	58	inex2 4545	. . . . . . . . . . . . . . . . . . . . 21
60	30, 59	eqeltri 2525	. . . . . . . . . . . . . . . . . . . 20
61	60	cnvex 6740	. . . . . . . . . . . . . . . . . . 19
62		imaexg 6730	. . . . . . . . . . . . . . . . . . 19
63	61, 62	ax-mp 5	. . . . . . . . . . . . . . . . . 18
64	63	f1oen 7590	. . . . . . . . . . . . . . . . 17
65	46, 57, 64	3syl 18	. . . . . . . . . . . . . . . 16 $/\$
66		sseqin2 3651	. . . . . . . . . . . . . . . . . . 19
67	55, 66	mpbi 212	. . . . . . . . . . . . . . . . . 18
68	67	imaeq2i 5166	. . . . . . . . . . . . . . . . 17
69		isocnv 6221	. . . . . . . . . . . . . . . . . . . 20
70	46, 69	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$
71		simpr 463	. . . . . . . . . . . . . . . . . . 19 $/\$
72		isoini 6229	. . . . . . . . . . . . . . . . . . 19 $/\$
73	70, 71, 72	syl2anc 667	. . . . . . . . . . . . . . . . . 18 $/\$
74		fvex 5875	. . . . . . . . . . . . . . . . . . . . 21
75	74	epini 5198	. . . . . . . . . . . . . . . . . . . 20
76	75	ineq2i 3631	. . . . . . . . . . . . . . . . . . 19
77	34	oicl 8044	. . . . . . . . . . . . . . . . . . . . 21
78		f1of 5814	. . . . . . . . . . . . . . . . . . . . . . 23
79	36, 37, 38, 78	4syl 19	. . . . . . . . . . . . . . . . . . . . . 22
80	79	ffvelrnda 6022	. . . . . . . . . . . . . . . . . . . . 21 $/\$
81		ordelss 5439	. . . . . . . . . . . . . . . . . . . . 21 $/\$
82	77, 80, 81	sylancr 669	. . . . . . . . . . . . . . . . . . . 20 $/\$
83		dfss1 3637	. . . . . . . . . . . . . . . . . . . 20
84	82, 83	sylib 200	. . . . . . . . . . . . . . . . . . 19 $/\$
85	76, 84	syl5eq 2497	. . . . . . . . . . . . . . . . . 18 $/\$
86	73, 85	eqtrd 2485	. . . . . . . . . . . . . . . . 17 $/\$
87	68, 86	syl5eqr 2499	. . . . . . . . . . . . . . . 16 $/\$
88	65, 87	breqtrd 4427	. . . . . . . . . . . . . . 15 $/\$
89	88	ensymd 7620	. . . . . . . . . . . . . 14 $/\$
90		infxpen.3	. . . . . . . . . . . . . . . . . . 19
91		fvex 5875	. . . . . . . . . . . . . . . . . . . 20
92		fvex 5875	. . . . . . . . . . . . . . . . . . . 20
93	91, 92	unex 6589	. . . . . . . . . . . . . . . . . . 19
94	90, 93	eqeltri 2525	. . . . . . . . . . . . . . . . . 18
95	94	sucex 6638	. . . . . . . . . . . . . . . . 17
96	95, 95	xpex 6595	. . . . . . . . . . . . . . . 16
97		xpss 4941	. . . . . . . . . . . . . . . . . . . 20
98		simp3 1010	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
99		vex 3048	. . . . . . . . . . . . . . . . . . . . . . 23
100		vex 3048	. . . . . . . . . . . . . . . . . . . . . . . 24
101	100	eliniseg 5197	. . . . . . . . . . . . . . . . . . . . . . 23
102	99, 101	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
103	98, 102	sylib 200	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
104	30	breqi 4408	. . . . . . . . . . . . . . . . . . . . . . 23
105		brin 4452	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
106	104, 105	bitri 253	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
107	106	simprbi 466	. . . . . . . . . . . . . . . . . . . . 21
108		brxp 4865	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
109	108	simplbi 462	. . . . . . . . . . . . . . . . . . . . 21
110	103, 107, 109	3syl 18	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
111	97, 110	sseldi 3430	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
112	17	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
113	112	3adant3 1028	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
114		xp1st 6823	. . . . . . . . . . . . . . . . . . . . . 22
115		onelon 5448	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
116	114, 115	sylan2 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$
117	113, 110, 116	syl2anc 667	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
118		eloni 5433	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119		elxp7 6826	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
120	119	simprbi 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
121		ordunel 6654	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
122	121	3expib 1211	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
123	118, 120, 122	syl2im 39	. . . . . . . . . . . . . . . . . . . . . . . . 25
124	112, 71, 123	sylc 62	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
125	90, 124	syl5eqel 2533	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
126		simprr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
127	13, 126	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . 26
128		simprl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
129	13, 128	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130		iscard 8409	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131		cardlim 8406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
132		sseq2 3454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133		limeq 5435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
134	132, 133	bibi12d 323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
135	131, 134	mpbii 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136	130, 135	sylbir 217	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
137	136	biimpa 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
138	17, 127, 129, 137	syl21anc 1267	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	138	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
140		limsuc 6676	. . . . . . . . . . . . . . . . . . . . . . . 24
141	139, 140	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
142	125, 141	mpbid 214	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
143		onelon 5448	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
144	112, 142, 143	syl2anc 667	. . . . . . . . . . . . . . . . . . . . 21 $/\$
145	144	3adant3 1028	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
146		ssun1 3597	. . . . . . . . . . . . . . . . . . . . 21
147	146	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
148	106	simplbi 462	. . . . . . . . . . . . . . . . . . . . 21
149		df-br 4403	. . . . . . . . . . . . . . . . . . . . . . . . . 26
150	23	eleq2i 2521	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$
151		opabid 4708	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
152	149, 150, 151	3bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\/$ $/\$
153	152	simprbi 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$ $/\$
154		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
155	154	orim2i 521	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$ $/\$ $\/$
156	153, 155	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
157		fvex 5875	. . . . . . . . . . . . . . . . . . . . . . . . 25
158		fvex 5875	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	157, 158	unex 6589	. . . . . . . . . . . . . . . . . . . . . . . 24
160	159	elsuc 5492	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
161	156, 160	sylibr 216	. . . . . . . . . . . . . . . . . . . . . 22
162		suceq 5488	. . . . . . . . . . . . . . . . . . . . . . 23
163	90, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
164	161, 163	syl6eleqr 2540	. . . . . . . . . . . . . . . . . . . . 21
165	103, 148, 164	3syl 18	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
166		ontr2 5470	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
167	166	imp 431	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
168	117, 145, 147, 165, 167	syl22anc 1269	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
169		xp2nd 6824	. . . . . . . . . . . . . . . . . . . . . 22
170		onelon 5448	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
171	169, 170	sylan2 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$
172	113, 110, 171	syl2anc 667	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
173		ssun2 3598	. . . . . . . . . . . . . . . . . . . . 21
174	173	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
175		ontr2 5470	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
176	175	imp 431	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
177	172, 145, 174, 165, 176	syl22anc 1269	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
178		elxp7 6826	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
179	178	biimpri 210	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
180	111, 168, 177, 179	syl12anc 1266	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
181	180	3expia 1210	. . . . . . . . . . . . . . . . 17 $/\$
182	181	ssrdv 3438	. . . . . . . . . . . . . . . 16 $/\$
183		ssdomg 7615	. . . . . . . . . . . . . . . 16
184	96, 182, 183	mpsyl 65	. . . . . . . . . . . . . . 15 $/\$
185	129	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
186		nnfi 7765	. . . . . . . . . . . . . . . . . . . 20
187		xpfi 7842	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
188	187	anidms 651	. . . . . . . . . . . . . . . . . . . . 21
189		isfinite 8157	. . . . . . . . . . . . . . . . . . . . 21
190	188, 189	sylib 200	. . . . . . . . . . . . . . . . . . . 20
191	186, 190	syl 17	. . . . . . . . . . . . . . . . . . 19
192		ssdomg 7615	. . . . . . . . . . . . . . . . . . . 20
193	14, 192	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
194		sdomdomtr 7705	. . . . . . . . . . . . . . . . . . 19 $/\$
195	191, 193, 194	syl2an 480	. . . . . . . . . . . . . . . . . 18 $/\$
196	195	expcom 437	. . . . . . . . . . . . . . . . 17
197	185, 196	syl 17	. . . . . . . . . . . . . . . 16 $/\$
198	127	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
199		breq1 4405	. . . . . . . . . . . . . . . . . . 19
200	199	rspccv 3147	. . . . . . . . . . . . . . . . . 18
201	198, 142, 200	sylc 62	. . . . . . . . . . . . . . . . 17 $/\$
202		omelon 8151	. . . . . . . . . . . . . . . . . . 19
203		ontri1 5457	. . . . . . . . . . . . . . . . . . 19 $/\$
204	202, 144, 203	sylancr 669	. . . . . . . . . . . . . . . . . 18 $/\$
205		simplr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
206	13, 205	sylbi 199	. . . . . . . . . . . . . . . . . . . 20
207	206	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$
208		sseq2 3454	. . . . . . . . . . . . . . . . . . . . 21
209		xpeq12 4853	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
210	209	anidms 651	. . . . . . . . . . . . . . . . . . . . . 22
211		id 22	. . . . . . . . . . . . . . . . . . . . . 22
212	210, 211	breq12d 4415	. . . . . . . . . . . . . . . . . . . . 21
213	208, 212	imbi12d 322	. . . . . . . . . . . . . . . . . . . 20
214	213	rspccv 3147	. . . . . . . . . . . . . . . . . . 19
215	207, 142, 214	sylc 62	. . . . . . . . . . . . . . . . . 18 $/\$
216	204, 215	sylbird 239	. . . . . . . . . . . . . . . . 17 $/\$
217		ensdomtr 7708	. . . . . . . . . . . . . . . . . 18 $/\$
218	217	expcom 437	. . . . . . . . . . . . . . . . 17
219	201, 216, 218	sylsyld 58	. . . . . . . . . . . . . . . 16 $/\$
220	197, 219	pm2.61d 162	. . . . . . . . . . . . . . 15 $/\$
221		domsdomtr 7707	. . . . . . . . . . . . . . 15 $/\$
222	184, 220, 221	syl2anc 667	. . . . . . . . . . . . . 14 $/\$
223		ensdomtr 7708	. . . . . . . . . . . . . 14 $/\$
224	89, 222, 223	syl2anc 667	. . . . . . . . . . . . 13 $/\$
225		ordelon 5447	. . . . . . . . . . . . . . 15 $/\$
226	77, 80, 225	sylancr 669	. . . . . . . . . . . . . 14 $/\$
227		onenon 8383	. . . . . . . . . . . . . . 15
228	112, 227	syl 17	. . . . . . . . . . . . . 14 $/\$
229		cardsdomel 8408	. . . . . . . . . . . . . 14 $/\$
230	226, 228, 229	syl2anc 667	. . . . . . . . . . . . 13 $/\$
231	224, 230	mpbid 214	. . . . . . . . . . . 12 $/\$
232		eleq2 2518	. . . . . . . . . . . . . 14
233	130, 232	sylbir 217	. . . . . . . . . . . . 13 $/\$
234	112, 198, 233	syl2anc 667	. . . . . . . . . . . 12 $/\$
235	231, 234	mpbid 214	. . . . . . . . . . 11 $/\$
236	235	ralrimiva 2802	. . . . . . . . . 10
237		fnfvrnss 6051	. . . . . . . . . . 11 $/\$
238		ssdomg 7615	. . . . . . . . . . 11
239	14, 237, 238	mpsyl 65	. . . . . . . . . 10 $/\$
240	45, 236, 239	syl2anc 667	. . . . . . . . 9
241		endomtr 7627	. . . . . . . . 9 $/\$
242	43, 240, 241	syl2anc 667	. . . . . . . 8
243	13, 242	sylbir 217	. . . . . . 7 $/\$ $/\$ $/\$
244		df1o2 7194	. . . . . . . . . . . 12
245		1onn 7340	. . . . . . . . . . . 12
246	244, 245	eqeltrri 2526	. . . . . . . . . . 11
247		nnsdom 8159	. . . . . . . . . . 11
248		sdomdom 7597	. . . . . . . . . . 11
249	246, 247, 248	mp2b 10	. . . . . . . . . 10
250		domtr 7622	. . . . . . . . . 10 $/\$
251	249, 193, 250	sylancr 669	. . . . . . . . 9
252		0ex 4535	. . . . . . . . . . . 12
253	14, 252	xpsnen 7656	. . . . . . . . . . 11
254	253	ensymi 7619	. . . . . . . . . 10
255	14	xpdom2 7667	. . . . . . . . . 10
256		endomtr 7627	. . . . . . . . . 10 $/\$
257	254, 255, 256	sylancr 669	. . . . . . . . 9
258	251, 257	syl 17	. . . . . . . 8
259	258	ad2antrl 734	. . . . . . 7 $/\$ $/\$ $/\$
260		sbth 7692	. . . . . . 7 $/\$
261	243, 259, 260	syl2anc 667	. . . . . 6 $/\$ $/\$ $/\$
262	261	expr 620	. . . . 5 $/\$ $/\$
263		simplr 762	. . . . . . . 8 $/\$ $/\$ $/\$
264		simpll 760	. . . . . . . . 9 $/\$ $/\$ $/\$
265		simprr 766	. . . . . . . . 9 $/\$ $/\$ $/\$
266		rexnal 2836	. . . . . . . . . 10
267		onelss 5465	. . . . . . . . . . . . 13
268		ssdomg 7615	. . . . . . . . . . . . 13
269	267, 268	syld 45	. . . . . . . . . . . 12
270		bren2 7600	. . . . . . . . . . . . 13 $/\$
271	270	simplbi2 631	. . . . . . . . . . . 12
272	269, 271	syl6 34	. . . . . . . . . . 11
273	272	reximdvai 2859	. . . . . . . . . 10
274	266, 273	syl5bir 222	. . . . . . . . 9
275	264, 265, 274	sylc 62	. . . . . . . 8 $/\$ $/\$ $/\$
276		r19.29 2925	. . . . . . . 8 $/\$ $/\$
277	263, 275, 276	syl2anc 667	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
278		simprl 764	. . . . . . . 8 $/\$ $/\$ $/\$
279		onelon 5448	. . . . . . . . . . . . . . . . 17 $/\$
280		ensym 7618	. . . . . . . . . . . . . . . . . 18
281		domentr 7628	. . . . . . . . . . . . . . . . . 18 $/\$
282	193, 280, 281	syl2an 480	. . . . . . . . . . . . . . . . 17 $/\$
283		domnsym 7698	. . . . . . . . . . . . . . . . . . 19
284		nnsdom 8159	. . . . . . . . . . . . . . . . . . 19
285	283, 284	nsyl 125	. . . . . . . . . . . . . . . . . 18
286		ontri1 5457	. . . . . . . . . . . . . . . . . . 19 $/\$
287	202, 286	mpan 676	. . . . . . . . . . . . . . . . . 18
288	285, 287	syl5ibr 225	. . . . . . . . . . . . . . . . 17
289	279, 282, 288	syl2im 39	. . . . . . . . . . . . . . . 16 $/\$ $/\$
290	289	expd 438	. . . . . . . . . . . . . . 15 $/\$
291	290	impcom 432	. . . . . . . . . . . . . 14 $/\$ $/\$
292	291	imim1d 78	. . . . . . . . . . . . 13 $/\$ $/\$
293	292	imp32 435	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
294		entr 7621	. . . . . . . . . . . . . . . 16 $/\$
295	294	ancoms 455	. . . . . . . . . . . . . . 15 $/\$
296		xpen 7735	. . . . . . . . . . . . . . . . . 18 $/\$
297	296	anidms 651	. . . . . . . . . . . . . . . . 17
298		entr 7621	. . . . . . . . . . . . . . . . 17 $/\$
299	297, 298	sylan 474	. . . . . . . . . . . . . . . 16 $/\$
300	280, 299	sylan 474	. . . . . . . . . . . . . . 15 $/\$
301	295, 300	syldan 473	. . . . . . . . . . . . . 14 $/\$
302	301	ex 436	. . . . . . . . . . . . 13
303	302	ad2antll 735	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
304	293, 303	mpd 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
305	304	ex 436	. . . . . . . . . 10 $/\$ $/\$ $/\$
306	305	expr 620	. . . . . . . . 9 $/\$ $/\$
307	306	rexlimdv 2877	. . . . . . . 8 $/\$ $/\$
308	278, 264, 307	syl2anc 667	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
309	277, 308	mpd 15	. . . . . 6 $/\$ $/\$ $/\$
310	309	expr 620	. . . . 5 $/\$ $/\$
311	262, 310	pm2.61d 162	. . . 4 $/\$ $/\$
312	311	exp31 609	. . 3
313	6, 12, 312	tfis3 6684	. 2
314	313	imp 431	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $/\$ w3a 985

wceq 1444

wcel 1887

wral 2737

wrex 2738

cvv 3045

cun 3402

cin 3403

wss 3404

c0 3731

csn 3968

cop 3974 class class class wbr 4402

copab 4460

cep 4743 Se wse 4791

wwe 4792

cxp 4832

ccnv 4833

cdm 4834

crn 4835

cres 4836

cima 4837

word 5422

con0 5423

wlim 5424

csuc 5425

wfn 5577

wf 5578

wf1 5579

wf1o 5581

cfv 5582

wiso 5583

com 6692

c1st 6791

c2nd 6792

c1o 7175

cen 7566

cdom 7567

csdm 7568

cfn 7569 OrdIsocoi 8024

ccrd 8369

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-inf2 8146

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-se 4794 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-oadd 7186 df-er 7363 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-oi 8025 df-card 8373

This theorem is referenced by: infxpen 8445

W3C validator