infxpenlem - Metamath Proof Explorer

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

Theorem infxpenlem 8290

Description: Lemma for infxpen 8291. (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 3485	. . . 4
2		xpeq12 4966	. . . . . 6 $/\$
3	2	anidms 645	. . . . 5
4		id 22	. . . . 5
5	3, 4	breq12d 4412	. . . 4
6	1, 5	imbi12d 320	. . 3
7		sseq2 3485	. . . 4
8		xpeq12 4966	. . . . . 6 $/\$
9	8	anidms 645	. . . . 5
10		id 22	. . . . 5
11	9, 10	breq12d 4412	. . . 4
12	7, 11	imbi12d 320	. . 3
13		infxpen.2	. . . . . . . 8 $/\$ $/\$ $/\$
14		vex 3079	. . . . . . . . . . . . 13
15	14, 14	xpex 6617	. . . . . . . . . . . 12
16		simpll 753	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
17	13, 16	sylbi 195	. . . . . . . . . . . . . . . . 17
18		onss 6511	. . . . . . . . . . . . . . . . 17
19	17, 18	syl 16	. . . . . . . . . . . . . . . 16
20		xpss12 5052	. . . . . . . . . . . . . . . 16 $/\$
21	19, 19, 20	syl2anc 661	. . . . . . . . . . . . . . 15
22		leweon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
23		r0weon.1	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
24	22, 23	r0weon 8289	. . . . . . . . . . . . . . . 16 $/\$ Se
25	24	simpli 458	. . . . . . . . . . . . . . 15
26		wess 4814	. . . . . . . . . . . . . . 15
27	21, 25, 26	mpisyl 18	. . . . . . . . . . . . . 14
28		weinxp 5013	. . . . . . . . . . . . . 14
29	27, 28	sylib 196	. . . . . . . . . . . . 13
30		infxpen.1	. . . . . . . . . . . . . 14
31		weeq1 4815	. . . . . . . . . . . . . 14
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13
33	29, 32	sylibr 212	. . . . . . . . . . . 12
34		infxpen.4	. . . . . . . . . . . . 13 OrdIso
35	34	oiiso 7861	. . . . . . . . . . . 12 $/\$
36	15, 33, 35	sylancr 663	. . . . . . . . . . 11
37		isof1o 6124	. . . . . . . . . . 11
38		f1ocnv 5760	. . . . . . . . . . 11
39		f1of1 5747	. . . . . . . . . . 11
40	36, 37, 38, 39	4syl 21	. . . . . . . . . 10
41		f1f1orn 5759	. . . . . . . . . 10
42	15	f1oen 7439	. . . . . . . . . 10
43	40, 41, 42	3syl 20	. . . . . . . . 9
44		f1ofn 5749	. . . . . . . . . . 11
45	36, 37, 38, 44	4syl 21	. . . . . . . . . 10
46	36	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
47	37, 38, 39	3syl 20	. . . . . . . . . . . . . . . . . 18
48		cnvimass 5296	. . . . . . . . . . . . . . . . . . 19
49		inss2 3678	. . . . . . . . . . . . . . . . . . . . . 22
50	30, 49	eqsstri 3493	. . . . . . . . . . . . . . . . . . . . 21
51		dmss 5146	. . . . . . . . . . . . . . . . . . . . 21
52	50, 51	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
53		dmxpid 5166	. . . . . . . . . . . . . . . . . . . 20
54	52, 53	sseqtri 3495	. . . . . . . . . . . . . . . . . . 19
55	48, 54	sstri 3472	. . . . . . . . . . . . . . . . . 18
56		f1ores 5762	. . . . . . . . . . . . . . . . . 18 $/\$
57	47, 55, 56	sylancl 662	. . . . . . . . . . . . . . . . 17
58	15, 15	xpex 6617	. . . . . . . . . . . . . . . . . . . . . 22
59	58	inex2 4541	. . . . . . . . . . . . . . . . . . . . 21
60	30, 59	eqeltri 2538	. . . . . . . . . . . . . . . . . . . 20
61	60	cnvex 6634	. . . . . . . . . . . . . . . . . . 19
62		imaexg 6624	. . . . . . . . . . . . . . . . . . 19
63	61, 62	ax-mp 5	. . . . . . . . . . . . . . . . . 18
64	63	f1oen 7439	. . . . . . . . . . . . . . . . 17
65	46, 57, 64	3syl 20	. . . . . . . . . . . . . . . 16 $/\$
66		sseqin2 3676	. . . . . . . . . . . . . . . . . . 19
67	55, 66	mpbi 208	. . . . . . . . . . . . . . . . . 18
68	67	imaeq2i 5274	. . . . . . . . . . . . . . . . 17
69		isocnv 6129	. . . . . . . . . . . . . . . . . . . 20
70	46, 69	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$
71		simpr 461	. . . . . . . . . . . . . . . . . . 19 $/\$
72		isoini 6137	. . . . . . . . . . . . . . . . . . 19 $/\$
73	70, 71, 72	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$
74		fvex 5808	. . . . . . . . . . . . . . . . . . . . 21
75	74	epini 5306	. . . . . . . . . . . . . . . . . . . 20
76	75	ineq2i 3656	. . . . . . . . . . . . . . . . . . 19
77	34	oicl 7853	. . . . . . . . . . . . . . . . . . . . 21
78		f1of 5748	. . . . . . . . . . . . . . . . . . . . . . 23
79	36, 37, 38, 78	4syl 21	. . . . . . . . . . . . . . . . . . . . . 22
80	79	ffvelrnda 5951	. . . . . . . . . . . . . . . . . . . . 21 $/\$
81		ordelss 4842	. . . . . . . . . . . . . . . . . . . . 21 $/\$
82	77, 80, 81	sylancr 663	. . . . . . . . . . . . . . . . . . . 20 $/\$
83		dfss1 3662	. . . . . . . . . . . . . . . . . . . 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 4423	. . . . . . . . . . . . . . 15 $/\$
89	88	ensymd 7469	. . . . . . . . . . . . . 14 $/\$
90		infxpen.3	. . . . . . . . . . . . . . . . . . 19
91		fvex 5808	. . . . . . . . . . . . . . . . . . . 20
92		fvex 5808	. . . . . . . . . . . . . . . . . . . 20
93	91, 92	unex 6487	. . . . . . . . . . . . . . . . . . 19
94	90, 93	eqeltri 2538	. . . . . . . . . . . . . . . . . 18
95	94	sucex 6531	. . . . . . . . . . . . . . . . 17
96	95, 95	xpex 6617	. . . . . . . . . . . . . . . 16
97		xpss 5053	. . . . . . . . . . . . . . . . . . . 20
98		simp3 990	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
99		vex 3079	. . . . . . . . . . . . . . . . . . . . . . 23
100		vex 3079	. . . . . . . . . . . . . . . . . . . . . . . 24
101	100	eliniseg 5305	. . . . . . . . . . . . . . . . . . . . . . 23
102	99, 101	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
103	98, 102	sylib 196	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
104	30	breqi 4405	. . . . . . . . . . . . . . . . . . . . . . 23
105		brin 4448	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
106	104, 105	bitri 249	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
107	106	simprbi 464	. . . . . . . . . . . . . . . . . . . . 21
108		brxp 4977	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
109	108	simplbi 460	. . . . . . . . . . . . . . . . . . . . 21
110	103, 107, 109	3syl 20	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
111	97, 110	sseldi 3461	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
112	17	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
113	112	3adant3 1008	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
114		xp1st 6715	. . . . . . . . . . . . . . . . . . . . . 22
115		onelon 4851	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
116	114, 115	sylan2 474	. . . . . . . . . . . . . . . . . . . . 21 $/\$
117	113, 110, 116	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
118		eloni 4836	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119		elxp7 6718	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
120	119	simprbi 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
121		ordunel 6547	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
122	121	3expib 1191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
123	118, 120, 122	syl2im 38	. . . . . . . . . . . . . . . . . . . . . . . . 25
124	112, 71, 123	sylc 60	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
125	90, 124	syl5eqel 2546	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
126		simprr 756	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
127	13, 126	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
128		simprl 755	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
129	13, 128	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130		iscard 8255	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131		cardlim 8252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
132		sseq2 3485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133		limeq 4838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1218	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	138	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
140		limsuc 6569	. . . . . . . . . . . . . . . . . . . . . . . 24
141	139, 140	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
142	125, 141	mpbid 210	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
143		onelon 4851	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
144	112, 142, 143	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$
145	144	3adant3 1008	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
146		ssun1 3626	. . . . . . . . . . . . . . . . . . . . 21
147	146	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
148	106	simplbi 460	. . . . . . . . . . . . . . . . . . . . 21
149		df-br 4400	. . . . . . . . . . . . . . . . . . . . . . . . . 26
150	23	eleq2i 2532	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$
151		opabid 4703	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5808	. . . . . . . . . . . . . . . . . . . . . . . . 25
158		fvex 5808	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	157, 158	unex 6487	. . . . . . . . . . . . . . . . . . . . . . . 24
160	159	elsuc 4895	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
161	156, 160	sylibr 212	. . . . . . . . . . . . . . . . . . . . . 22
162		suceq 4891	. . . . . . . . . . . . . . . . . . . . . . 23
163	90, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
164	161, 163	syl6eleqr 2553	. . . . . . . . . . . . . . . . . . . . 21
165	103, 148, 164	3syl 20	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
166		ontr2 4873	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
167	166	imp 429	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
168	117, 145, 147, 165, 167	syl22anc 1220	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
169		xp2nd 6716	. . . . . . . . . . . . . . . . . . . . . 22
170		onelon 4851	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
171	169, 170	sylan2 474	. . . . . . . . . . . . . . . . . . . . 21 $/\$
172	113, 110, 171	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
173		ssun2 3627	. . . . . . . . . . . . . . . . . . . . 21
174	173	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
175		ontr2 4873	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
176	175	imp 429	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
177	172, 145, 174, 165, 176	syl22anc 1220	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
178		elxp7 6718	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
179	178	biimpri 206	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
180	111, 168, 177, 179	syl12anc 1217	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
181	180	3expia 1190	. . . . . . . . . . . . . . . . 17 $/\$
182	181	ssrdv 3469	. . . . . . . . . . . . . . . 16 $/\$
183		ssdomg 7464	. . . . . . . . . . . . . . . 16
184	96, 182, 183	mpsyl 63	. . . . . . . . . . . . . . 15 $/\$
185	129	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
186		nnfi 7613	. . . . . . . . . . . . . . . . . . . 20
187		xpfi 7693	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
188	187	anidms 645	. . . . . . . . . . . . . . . . . . . . 21
189		isfinite 7968	. . . . . . . . . . . . . . . . . . . . 21
190	188, 189	sylib 196	. . . . . . . . . . . . . . . . . . . 20
191	186, 190	syl 16	. . . . . . . . . . . . . . . . . . 19
192		ssdomg 7464	. . . . . . . . . . . . . . . . . . . 20
193	14, 192	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
194		sdomdomtr 7553	. . . . . . . . . . . . . . . . . . 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 4402	. . . . . . . . . . . . . . . . . . 19
200	199	rspccv 3174	. . . . . . . . . . . . . . . . . 18
201	198, 142, 200	sylc 60	. . . . . . . . . . . . . . . . 17 $/\$
202		omelon 7962	. . . . . . . . . . . . . . . . . . 19
203		ontri1 4860	. . . . . . . . . . . . . . . . . . 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 3485	. . . . . . . . . . . . . . . . . . . . 21
209		xpeq12 4966	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
210	209	anidms 645	. . . . . . . . . . . . . . . . . . . . . 22
211		id 22	. . . . . . . . . . . . . . . . . . . . . 22
212	210, 211	breq12d 4412	. . . . . . . . . . . . . . . . . . . . 21
213	208, 212	imbi12d 320	. . . . . . . . . . . . . . . . . . . 20
214	213	rspccv 3174	. . . . . . . . . . . . . . . . . . 19
215	207, 142, 214	sylc 60	. . . . . . . . . . . . . . . . . 18 $/\$
216	204, 215	sylbird 235	. . . . . . . . . . . . . . . . 17 $/\$
217		ensdomtr 7556	. . . . . . . . . . . . . . . . . 18 $/\$
218	217	expcom 435	. . . . . . . . . . . . . . . . 17
219	201, 216, 218	sylsyld 56	. . . . . . . . . . . . . . . 16 $/\$
220	197, 219	pm2.61d 158	. . . . . . . . . . . . . . 15 $/\$
221		domsdomtr 7555	. . . . . . . . . . . . . . 15 $/\$
222	184, 220, 221	syl2anc 661	. . . . . . . . . . . . . 14 $/\$
223		ensdomtr 7556	. . . . . . . . . . . . . 14 $/\$
224	89, 222, 223	syl2anc 661	. . . . . . . . . . . . 13 $/\$
225		ordelon 4850	. . . . . . . . . . . . . . 15 $/\$
226	77, 80, 225	sylancr 663	. . . . . . . . . . . . . 14 $/\$
227		onenon 8229	. . . . . . . . . . . . . . 15
228	112, 227	syl 16	. . . . . . . . . . . . . 14 $/\$
229		cardsdomel 8254	. . . . . . . . . . . . . 14 $/\$
230	226, 228, 229	syl2anc 661	. . . . . . . . . . . . 13 $/\$
231	224, 230	mpbid 210	. . . . . . . . . . . 12 $/\$
232		eleq2 2527	. . . . . . . . . . . . . 14
233	130, 232	sylbir 213	. . . . . . . . . . . . 13 $/\$
234	112, 198, 233	syl2anc 661	. . . . . . . . . . . 12 $/\$
235	231, 234	mpbid 210	. . . . . . . . . . 11 $/\$
236	235	ralrimiva 2829	. . . . . . . . . 10
237		fnfvrnss 5979	. . . . . . . . . . 11 $/\$
238		ssdomg 7464	. . . . . . . . . . 11
239	14, 237, 238	mpsyl 63	. . . . . . . . . 10 $/\$
240	45, 236, 239	syl2anc 661	. . . . . . . . 9
241		endomtr 7476	. . . . . . . . 9 $/\$
242	43, 240, 241	syl2anc 661	. . . . . . . 8
243	13, 242	sylbir 213	. . . . . . 7 $/\$ $/\$ $/\$
244		df1o2 7041	. . . . . . . . . . . 12
245		1onn 7187	. . . . . . . . . . . 12
246	244, 245	eqeltrri 2539	. . . . . . . . . . 11
247		nnsdom 7969	. . . . . . . . . . 11
248		sdomdom 7446	. . . . . . . . . . 11
249	246, 247, 248	mp2b 10	. . . . . . . . . 10
250		domtr 7471	. . . . . . . . . 10 $/\$
251	249, 193, 250	sylancr 663	. . . . . . . . 9
252		0ex 4529	. . . . . . . . . . . 12
253	14, 252	xpsnen 7504	. . . . . . . . . . 11
254	253	ensymi 7468	. . . . . . . . . 10
255	14	xpdom2 7515	. . . . . . . . . 10
256		endomtr 7476	. . . . . . . . . 10 $/\$
257	254, 255, 256	sylancr 663	. . . . . . . . 9
258	251, 257	syl 16	. . . . . . . 8
259	258	ad2antrl 727	. . . . . . 7 $/\$ $/\$ $/\$
260		sbth 7540	. . . . . . 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 2853	. . . . . . . . . 10
267		onelss 4868	. . . . . . . . . . . . 13
268		ssdomg 7464	. . . . . . . . . . . . 13
269	267, 268	syld 44	. . . . . . . . . . . 12
270		bren2 7449	. . . . . . . . . . . . 13 $/\$
271	270	simplbi2 625	. . . . . . . . . . . 12
272	269, 271	syl6 33	. . . . . . . . . . 11
273	272	reximdvai 2930	. . . . . . . . . 10
274	266, 273	syl5bir 218	. . . . . . . . 9
275	264, 265, 274	sylc 60	. . . . . . . 8 $/\$ $/\$ $/\$
276		r19.29 2961	. . . . . . . 8 $/\$ $/\$
277	263, 275, 276	syl2anc 661	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
278		simprl 755	. . . . . . . 8 $/\$ $/\$ $/\$
279		onelon 4851	. . . . . . . . . . . . . . . . 17 $/\$
280		ensym 7467	. . . . . . . . . . . . . . . . . 18
281		domentr 7477	. . . . . . . . . . . . . . . . . 18 $/\$
282	193, 280, 281	syl2an 477	. . . . . . . . . . . . . . . . 17 $/\$
283		domnsym 7546	. . . . . . . . . . . . . . . . . . 19
284		nnsdom 7969	. . . . . . . . . . . . . . . . . . 19
285	283, 284	nsyl 121	. . . . . . . . . . . . . . . . . 18
286		ontri1 4860	. . . . . . . . . . . . . . . . . . 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 7470	. . . . . . . . . . . . . . . 16 $/\$
295	294	ancoms 453	. . . . . . . . . . . . . . 15 $/\$
296		xpen 7583	. . . . . . . . . . . . . . . . . 18 $/\$
297	296	anidms 645	. . . . . . . . . . . . . . . . 17
298		entr 7470	. . . . . . . . . . . . . . . . 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 2944	. . . . . . . 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 6577	. 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 965

wceq 1370

wcel 1758

wral 2798

wrex 2799

cvv 3076

cun 3433

cin 3434

wss 3435

c0 3744

csn 3984

cop 3990 class class class wbr 4399

copab 4456

cep 4737 Se wse 4784

wwe 4785

word 4825

con0 4826

wlim 4827

csuc 4828

cxp 4945

ccnv 4946

cdm 4947

crn 4948

cres 4949

cima 4950

wfn 5520

wf 5521

wf1 5522

wf1o 5524

cfv 5525

wiso 5526

com 6585

c1st 6684

c2nd 6685

c1o 7022

cen 7416

cdom 7417

csdm 7418

cfn 7419 OrdIsocoi 7833

ccrd 8215

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4510 ax-sep 4520 ax-nul 4528 ax-pow 4577 ax-pr 4638 ax-un 6481 ax-inf2 7957

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2649 df-ral 2803 df-rex 2804 df-reu 2805 df-rmo 2806 df-rab 2807 df-v 3078 df-sbc 3293 df-csb 3395 df-dif 3438 df-un 3440 df-in 3442 df-ss 3449 df-pss 3451 df-nul 3745 df-if 3899 df-pw 3969 df-sn 3985 df-pr 3987 df-tp 3989 df-op 3991 df-uni 4199 df-int 4236 df-iun 4280 df-br 4400 df-opab 4458 df-mpt 4459 df-tr 4493 df-eprel 4739 df-id 4743 df-po 4748 df-so 4749 df-fr 4786 df-se 4787 df-we 4788 df-ord 4829 df-on 4830 df-lim 4831 df-suc 4832 df-xp 4953 df-rel 4954 df-cnv 4955 df-co 4956 df-dm 4957 df-rn 4958 df-res 4959 df-ima 4960 df-iota 5488 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-isom 5534 df-riota 6160 df-ov 6202 df-oprab 6203 df-mpt2 6204 df-om 6586 df-1st 6686 df-2nd 6687 df-recs 6941 df-rdg 6975 df-1o 7029 df-oadd 7033 df-er 7210 df-en 7420 df-dom 7421 df-sdom 7422 df-fin 7423 df-oi 7834 df-card 8219

This theorem is referenced by: infxpen 8291

W3C validator