infxpenlem - Metamath Proof Explorer

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

Theorem infxpenlem 8394

Description: Lemma for infxpen 8395. (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 5008	. . . . . 6 $/\$
3	2	anidms 645	. . . . 5
4		id 22	. . . . 5
5	3, 4	breq12d 4450	. . . 4
6	1, 5	imbi12d 320	. . 3
7		sseq2 3511	. . . 4
8		xpeq12 5008	. . . . . 6 $/\$
9	8	anidms 645	. . . . 5
10		id 22	. . . . 5
11	9, 10	breq12d 4450	. . . 4
12	7, 11	imbi12d 320	. . 3
13		infxpen.2	. . . . . . . 8 $/\$ $/\$ $/\$
14		vex 3098	. . . . . . . . . . . . 13
15	14, 14	xpex 6589	. . . . . . . . . . . 12
16		simpll 753	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
17	13, 16	sylbi 195	. . . . . . . . . . . . . . . . 17
18		onss 6611	. . . . . . . . . . . . . . . . 17
19	17, 18	syl 16	. . . . . . . . . . . . . . . 16
20		xpss12 5098	. . . . . . . . . . . . . . . 16 $/\$
21	19, 19, 20	syl2anc 661	. . . . . . . . . . . . . . 15
22		leweon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
23		r0weon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
24	22, 23	r0weon 8393	. . . . . . . . . . . . . . . 16 $/\$ Se
25	24	simpli 458	. . . . . . . . . . . . . . 15
26		wess 4856	. . . . . . . . . . . . . . 15
27	21, 25, 26	mpisyl 18	. . . . . . . . . . . . . 14
28		weinxp 5057	. . . . . . . . . . . . . 14
29	27, 28	sylib 196	. . . . . . . . . . . . 13
30		infxpen.1	. . . . . . . . . . . . . 14
31		weeq1 4857	. . . . . . . . . . . . . 14
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13
33	29, 32	sylibr 212	. . . . . . . . . . . 12
34		infxpen.4	. . . . . . . . . . . . 13 OrdIso
35	34	oiiso 7965	. . . . . . . . . . . 12 $/\$
36	15, 33, 35	sylancr 663	. . . . . . . . . . 11
37		isof1o 6206	. . . . . . . . . . 11
38		f1ocnv 5818	. . . . . . . . . . 11
39		f1of1 5805	. . . . . . . . . . 11
40	36, 37, 38, 39	4syl 21	. . . . . . . . . 10
41		f1f1orn 5817	. . . . . . . . . 10
42	15	f1oen 7538	. . . . . . . . . 10
43	40, 41, 42	3syl 20	. . . . . . . . 9
44		f1ofn 5807	. . . . . . . . . . 11
45	36, 37, 38, 44	4syl 21	. . . . . . . . . 10
46	36	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
47	37, 38, 39	3syl 20	. . . . . . . . . . . . . . . . . 18
48		cnvimass 5347	. . . . . . . . . . . . . . . . . . 19
49		inss2 3704	. . . . . . . . . . . . . . . . . . . . . 22
50	30, 49	eqsstri 3519	. . . . . . . . . . . . . . . . . . . . 21
51		dmss 5192	. . . . . . . . . . . . . . . . . . . . 21
52	50, 51	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
53		dmxpid 5212	. . . . . . . . . . . . . . . . . . . 20
54	52, 53	sseqtri 3521	. . . . . . . . . . . . . . . . . . 19
55	48, 54	sstri 3498	. . . . . . . . . . . . . . . . . 18
56		f1ores 5820	. . . . . . . . . . . . . . . . . 18 $/\$
57	47, 55, 56	sylancl 662	. . . . . . . . . . . . . . . . 17
58	15, 15	xpex 6589	. . . . . . . . . . . . . . . . . . . . . 22
59	58	inex2 4579	. . . . . . . . . . . . . . . . . . . . 21
60	30, 59	eqeltri 2527	. . . . . . . . . . . . . . . . . . . 20
61	60	cnvex 6732	. . . . . . . . . . . . . . . . . . 19
62		imaexg 6722	. . . . . . . . . . . . . . . . . . 19
63	61, 62	ax-mp 5	. . . . . . . . . . . . . . . . . 18
64	63	f1oen 7538	. . . . . . . . . . . . . . . . 17
65	46, 57, 64	3syl 20	. . . . . . . . . . . . . . . 16 $/\$
66		sseqin2 3702	. . . . . . . . . . . . . . . . . . 19
67	55, 66	mpbi 208	. . . . . . . . . . . . . . . . . 18
68	67	imaeq2i 5325	. . . . . . . . . . . . . . . . 17
69		isocnv 6211	. . . . . . . . . . . . . . . . . . . 20
70	46, 69	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$
71		simpr 461	. . . . . . . . . . . . . . . . . . 19 $/\$
72		isoini 6219	. . . . . . . . . . . . . . . . . . 19 $/\$
73	70, 71, 72	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$
74		fvex 5866	. . . . . . . . . . . . . . . . . . . . 21
75	74	epini 5357	. . . . . . . . . . . . . . . . . . . 20
76	75	ineq2i 3682	. . . . . . . . . . . . . . . . . . 19
77	34	oicl 7957	. . . . . . . . . . . . . . . . . . . . 21
78		f1of 5806	. . . . . . . . . . . . . . . . . . . . . . 23
79	36, 37, 38, 78	4syl 21	. . . . . . . . . . . . . . . . . . . . . 22
80	79	ffvelrnda 6016	. . . . . . . . . . . . . . . . . . . . 21 $/\$
81		ordelss 4884	. . . . . . . . . . . . . . . . . . . . 21 $/\$
82	77, 80, 81	sylancr 663	. . . . . . . . . . . . . . . . . . . 20 $/\$
83		dfss1 3688	. . . . . . . . . . . . . . . . . . . 20
84	82, 83	sylib 196	. . . . . . . . . . . . . . . . . . 19 $/\$
85	76, 84	syl5eq 2496	. . . . . . . . . . . . . . . . . 18 $/\$
86	73, 85	eqtrd 2484	. . . . . . . . . . . . . . . . 17 $/\$
87	68, 86	syl5eqr 2498	. . . . . . . . . . . . . . . 16 $/\$
88	65, 87	breqtrd 4461	. . . . . . . . . . . . . . 15 $/\$
89	88	ensymd 7568	. . . . . . . . . . . . . 14 $/\$
90		infxpen.3	. . . . . . . . . . . . . . . . . . 19
91		fvex 5866	. . . . . . . . . . . . . . . . . . . 20
92		fvex 5866	. . . . . . . . . . . . . . . . . . . 20
93	91, 92	unex 6583	. . . . . . . . . . . . . . . . . . 19
94	90, 93	eqeltri 2527	. . . . . . . . . . . . . . . . . 18
95	94	sucex 6631	. . . . . . . . . . . . . . . . 17
96	95, 95	xpex 6589	. . . . . . . . . . . . . . . 16
97		xpss 5099	. . . . . . . . . . . . . . . . . . . 20
98		simp3 999	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
99		vex 3098	. . . . . . . . . . . . . . . . . . . . . . 23
100		vex 3098	. . . . . . . . . . . . . . . . . . . . . . . 24
101	100	eliniseg 5356	. . . . . . . . . . . . . . . . . . . . . . 23
102	99, 101	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
103	98, 102	sylib 196	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
104	30	breqi 4443	. . . . . . . . . . . . . . . . . . . . . . 23
105		brin 4486	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
106	104, 105	bitri 249	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
107	106	simprbi 464	. . . . . . . . . . . . . . . . . . . . 21
108		brxp 5020	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
109	108	simplbi 460	. . . . . . . . . . . . . . . . . . . . 21
110	103, 107, 109	3syl 20	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
111	97, 110	sseldi 3487	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
112	17	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
113	112	3adant3 1017	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
114		xp1st 6815	. . . . . . . . . . . . . . . . . . . . . 22
115		onelon 4893	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
116	114, 115	sylan2 474	. . . . . . . . . . . . . . . . . . . . 21 $/\$
117	113, 110, 116	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
118		eloni 4878	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119		elxp7 6818	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
120	119	simprbi 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
121		ordunel 6647	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
122	121	3expib 1200	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
123	118, 120, 122	syl2im 38	. . . . . . . . . . . . . . . . . . . . . . . . 25
124	112, 71, 123	sylc 60	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
125	90, 124	syl5eqel 2535	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
126		simprr 757	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
127	13, 126	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
128		simprl 756	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
129	13, 128	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130		iscard 8359	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131		cardlim 8356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
132		sseq2 3511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133		limeq 4880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1228	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	138	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
140		limsuc 6669	. . . . . . . . . . . . . . . . . . . . . . . 24
141	139, 140	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
142	125, 141	mpbid 210	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
143		onelon 4893	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
144	112, 142, 143	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$
145	144	3adant3 1017	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
146		ssun1 3652	. . . . . . . . . . . . . . . . . . . . 21
147	146	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
148	106	simplbi 460	. . . . . . . . . . . . . . . . . . . . 21
149		df-br 4438	. . . . . . . . . . . . . . . . . . . . . . . . . 26
150	23	eleq2i 2521	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$
151		opabid 4744	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5866	. . . . . . . . . . . . . . . . . . . . . . . . 25
158		fvex 5866	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	157, 158	unex 6583	. . . . . . . . . . . . . . . . . . . . . . . 24
160	159	elsuc 4937	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
161	156, 160	sylibr 212	. . . . . . . . . . . . . . . . . . . . . 22
162		suceq 4933	. . . . . . . . . . . . . . . . . . . . . . 23
163	90, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
164	161, 163	syl6eleqr 2542	. . . . . . . . . . . . . . . . . . . . 21
165	103, 148, 164	3syl 20	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
166		ontr2 4915	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
167	166	imp 429	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
168	117, 145, 147, 165, 167	syl22anc 1230	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
169		xp2nd 6816	. . . . . . . . . . . . . . . . . . . . . 22
170		onelon 4893	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
171	169, 170	sylan2 474	. . . . . . . . . . . . . . . . . . . . 21 $/\$
172	113, 110, 171	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
173		ssun2 3653	. . . . . . . . . . . . . . . . . . . . 21
174	173	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
175		ontr2 4915	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
176	175	imp 429	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
177	172, 145, 174, 165, 176	syl22anc 1230	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
178		elxp7 6818	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
179	178	biimpri 206	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
180	111, 168, 177, 179	syl12anc 1227	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
181	180	3expia 1199	. . . . . . . . . . . . . . . . 17 $/\$
182	181	ssrdv 3495	. . . . . . . . . . . . . . . 16 $/\$
183		ssdomg 7563	. . . . . . . . . . . . . . . 16
184	96, 182, 183	mpsyl 63	. . . . . . . . . . . . . . 15 $/\$
185	129	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
186		nnfi 7712	. . . . . . . . . . . . . . . . . . . 20
187		xpfi 7793	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
188	187	anidms 645	. . . . . . . . . . . . . . . . . . . . 21
189		isfinite 8072	. . . . . . . . . . . . . . . . . . . . 21
190	188, 189	sylib 196	. . . . . . . . . . . . . . . . . . . 20
191	186, 190	syl 16	. . . . . . . . . . . . . . . . . . 19
192		ssdomg 7563	. . . . . . . . . . . . . . . . . . . 20
193	14, 192	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
194		sdomdomtr 7652	. . . . . . . . . . . . . . . . . . 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 4440	. . . . . . . . . . . . . . . . . . 19
200	199	rspccv 3193	. . . . . . . . . . . . . . . . . 18
201	198, 142, 200	sylc 60	. . . . . . . . . . . . . . . . 17 $/\$
202		omelon 8066	. . . . . . . . . . . . . . . . . . 19
203		ontri1 4902	. . . . . . . . . . . . . . . . . . 19 $/\$
204	202, 144, 203	sylancr 663	. . . . . . . . . . . . . . . . . 18 $/\$
205		simplr 755	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
206	13, 205	sylbi 195	. . . . . . . . . . . . . . . . . . . 20
207	206	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
208		sseq2 3511	. . . . . . . . . . . . . . . . . . . . 21
209		xpeq12 5008	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
210	209	anidms 645	. . . . . . . . . . . . . . . . . . . . . 22
211		id 22	. . . . . . . . . . . . . . . . . . . . . 22
212	210, 211	breq12d 4450	. . . . . . . . . . . . . . . . . . . . 21
213	208, 212	imbi12d 320	. . . . . . . . . . . . . . . . . . . 20
214	213	rspccv 3193	. . . . . . . . . . . . . . . . . . 19
215	207, 142, 214	sylc 60	. . . . . . . . . . . . . . . . . 18 $/\$
216	204, 215	sylbird 235	. . . . . . . . . . . . . . . . 17 $/\$
217		ensdomtr 7655	. . . . . . . . . . . . . . . . . 18 $/\$
218	217	expcom 435	. . . . . . . . . . . . . . . . 17
219	201, 216, 218	sylsyld 56	. . . . . . . . . . . . . . . 16 $/\$
220	197, 219	pm2.61d 158	. . . . . . . . . . . . . . 15 $/\$
221		domsdomtr 7654	. . . . . . . . . . . . . . 15 $/\$
222	184, 220, 221	syl2anc 661	. . . . . . . . . . . . . 14 $/\$
223		ensdomtr 7655	. . . . . . . . . . . . . 14 $/\$
224	89, 222, 223	syl2anc 661	. . . . . . . . . . . . 13 $/\$
225		ordelon 4892	. . . . . . . . . . . . . . 15 $/\$
226	77, 80, 225	sylancr 663	. . . . . . . . . . . . . 14 $/\$
227		onenon 8333	. . . . . . . . . . . . . . 15
228	112, 227	syl 16	. . . . . . . . . . . . . 14 $/\$
229		cardsdomel 8358	. . . . . . . . . . . . . 14 $/\$
230	226, 228, 229	syl2anc 661	. . . . . . . . . . . . 13 $/\$
231	224, 230	mpbid 210	. . . . . . . . . . . 12 $/\$
232		eleq2 2516	. . . . . . . . . . . . . 14
233	130, 232	sylbir 213	. . . . . . . . . . . . 13 $/\$
234	112, 198, 233	syl2anc 661	. . . . . . . . . . . 12 $/\$
235	231, 234	mpbid 210	. . . . . . . . . . 11 $/\$
236	235	ralrimiva 2857	. . . . . . . . . 10
237		fnfvrnss 6044	. . . . . . . . . . 11 $/\$
238		ssdomg 7563	. . . . . . . . . . 11
239	14, 237, 238	mpsyl 63	. . . . . . . . . 10 $/\$
240	45, 236, 239	syl2anc 661	. . . . . . . . 9
241		endomtr 7575	. . . . . . . . 9 $/\$
242	43, 240, 241	syl2anc 661	. . . . . . . 8
243	13, 242	sylbir 213	. . . . . . 7 $/\$ $/\$ $/\$
244		df1o2 7144	. . . . . . . . . . . 12
245		1onn 7290	. . . . . . . . . . . 12
246	244, 245	eqeltrri 2528	. . . . . . . . . . 11
247		nnsdom 8073	. . . . . . . . . . 11
248		sdomdom 7545	. . . . . . . . . . 11
249	246, 247, 248	mp2b 10	. . . . . . . . . 10
250		domtr 7570	. . . . . . . . . 10 $/\$
251	249, 193, 250	sylancr 663	. . . . . . . . 9
252		0ex 4567	. . . . . . . . . . . 12
253	14, 252	xpsnen 7603	. . . . . . . . . . 11
254	253	ensymi 7567	. . . . . . . . . 10
255	14	xpdom2 7614	. . . . . . . . . 10
256		endomtr 7575	. . . . . . . . . 10 $/\$
257	254, 255, 256	sylancr 663	. . . . . . . . 9
258	251, 257	syl 16	. . . . . . . 8
259	258	ad2antrl 727	. . . . . . 7 $/\$ $/\$ $/\$
260		sbth 7639	. . . . . . 7 $/\$
261	243, 259, 260	syl2anc 661	. . . . . 6 $/\$ $/\$ $/\$
262	261	expr 615	. . . . 5 $/\$ $/\$
263		simplr 755	. . . . . . . 8 $/\$ $/\$ $/\$
264		simpll 753	. . . . . . . . 9 $/\$ $/\$ $/\$
265		simprr 757	. . . . . . . . 9 $/\$ $/\$ $/\$
266		rexnal 2891	. . . . . . . . . 10
267		onelss 4910	. . . . . . . . . . . . 13
268		ssdomg 7563	. . . . . . . . . . . . 13
269	267, 268	syld 44	. . . . . . . . . . . 12
270		bren2 7548	. . . . . . . . . . . . 13 $/\$
271	270	simplbi2 625	. . . . . . . . . . . 12
272	269, 271	syl6 33	. . . . . . . . . . 11
273	272	reximdvai 2915	. . . . . . . . . 10
274	266, 273	syl5bir 218	. . . . . . . . 9
275	264, 265, 274	sylc 60	. . . . . . . 8 $/\$ $/\$ $/\$
276		r19.29 2978	. . . . . . . 8 $/\$ $/\$
277	263, 275, 276	syl2anc 661	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
278		simprl 756	. . . . . . . 8 $/\$ $/\$ $/\$
279		onelon 4893	. . . . . . . . . . . . . . . . 17 $/\$
280		ensym 7566	. . . . . . . . . . . . . . . . . 18
281		domentr 7576	. . . . . . . . . . . . . . . . . 18 $/\$
282	193, 280, 281	syl2an 477	. . . . . . . . . . . . . . . . 17 $/\$
283		domnsym 7645	. . . . . . . . . . . . . . . . . . 19
284		nnsdom 8073	. . . . . . . . . . . . . . . . . . 19
285	283, 284	nsyl 121	. . . . . . . . . . . . . . . . . 18
286		ontri1 4902	. . . . . . . . . . . . . . . . . . 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 7569	. . . . . . . . . . . . . . . 16 $/\$
295	294	ancoms 453	. . . . . . . . . . . . . . 15 $/\$
296		xpen 7682	. . . . . . . . . . . . . . . . . 18 $/\$
297	296	anidms 645	. . . . . . . . . . . . . . . . 17
298		entr 7569	. . . . . . . . . . . . . . . . 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 2933	. . . . . . . 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 6677	. 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 974

wceq 1383

wcel 1804

wral 2793

wrex 2794

cvv 3095

cun 3459

cin 3460

wss 3461

c0 3770

csn 4014

cop 4020 class class class wbr 4437

copab 4494

cep 4779 Se wse 4826

wwe 4827

word 4867

con0 4868

wlim 4869

csuc 4870

cxp 4987

ccnv 4988

cdm 4989

crn 4990

cres 4991

cima 4992

wfn 5573

wf 5574

wf1 5575

wf1o 5577

cfv 5578

wiso 5579

com 6685

c1st 6783

c2nd 6784

c1o 7125

cen 7515

cdom 7516

csdm 7517

cfn 7518 OrdIsocoi 7937

ccrd 8319

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-rep 4548 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 ax-inf2 8061

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-int 4272 df-iun 4317 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-se 4829 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-isom 5587 df-riota 6242 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-om 6686 df-1st 6785 df-2nd 6786 df-recs 7044 df-rdg 7078 df-1o 7132 df-oadd 7136 df-er 7313 df-en 7519 df-dom 7520 df-sdom 7521 df-fin 7522 df-oi 7938 df-card 8323

This theorem is referenced by: infxpen 8395

W3C validator