eldioph2lem2 - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > eldioph2lem2		Structured version Unicode version

Theorem eldioph2lem2 29052

Description: Lemma for eldioph2 29053. Construct necessary renaming function for one direction. (Contributed by Stefan O'Rear, 8-Oct-2014.)

**Assertion**
Ref	Expression
eldioph2lem2	$/\$ $/\$ $/\$ $/\$

Distinct variable groups:

Proof of Theorem eldioph2lem2 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simplr 754	. . . 4 $/\$ $/\$ $/\$
2		fzfi 11786	. . . 4
3		difinf 7574	. . . 4 $/\$ $\$
4	1, 2, 3	sylancl 662	. . 3 $/\$ $/\$ $/\$ $\$
5		fzfi 11786	. . . 4
6		diffi 7535	. . . 4 $\$
7	5, 6	ax-mp 5	. . 3 $\$
8		isinffi 8154	. . 3 $\$ $/\$ $\$ $\$ $\$
9	4, 7, 8	sylancl 662	. 2 $/\$ $/\$ $/\$ $\$ $\$
10		f1f1orn 5647	. . . . . . . 8 $\$ $\$ $\$
11	10	adantl 466	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
12		f1oi 5671	. . . . . . . 8
13	12	a1i 11	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\$ $\$
14		incom 3538	. . . . . . . . 9 $\$ $\$
15		disjdif 3746	. . . . . . . . 9 $\$
16	14, 15	eqtri 2458	. . . . . . . 8 $\$
17	16	a1i 11	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
18		f1f 5601	. . . . . . . . . . . 12 $\$ $\$ $\$ $\$
19		frn 5560	. . . . . . . . . . . 12 $\$ $\$ $\$
20	18, 19	syl 16	. . . . . . . . . . 11 $\$ $\$ $\$
21	20	adantl 466	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
22		ssrin 3570	. . . . . . . . . 10 $\$ $\$
23	21, 22	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
24		incom 3538	. . . . . . . . . 10 $\$ $\$
25		disjdif 3746	. . . . . . . . . 10 $\$
26	24, 25	eqtri 2458	. . . . . . . . 9 $\$
27	23, 26	syl6sseq 3397	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\$ $\$
28		ss0 3663	. . . . . . . 8
29	27, 28	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\$ $\$
30		f1oun 5655	. . . . . . 7 $\$ $/\$ $/\$ $\$ $/\$ $\$
31	11, 13, 17, 29, 30	syl22anc 1219	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
32		f1of1 5635	. . . . . 6 $\$ $\$
33	31, 32	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
34		uncom 3495	. . . . . . 7 $\$ $\$
35		simplrr 760	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$ $\$
36		fzss2 11490	. . . . . . . . 9
37	35, 36	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\$ $\$
38		undif 3754	. . . . . . . 8 $\$
39	37, 38	sylib 196	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
40	34, 39	syl5eq 2482	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
41		f1eq2 5597	. . . . . 6 $\$ $\$
42	40, 41	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
43	33, 42	mpbid 210	. . . 4 $/\$ $/\$ $/\$ $/\$ $\$ $\$
44	20	difss2d 3481	. . . . . 6 $\$ $\$
45	44	adantl 466	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\$ $\$
46		simplrl 759	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\$ $\$
47	45, 46	unssd 3527	. . . 4 $/\$ $/\$ $/\$ $/\$ $\$ $\$
48		f1ss 5606	. . . 4 $/\$
49	43, 47, 48	syl2anc 661	. . 3 $/\$ $/\$ $/\$ $/\$ $\$ $\$
50		resundir 5120	. . . 4
51		dmres 5126	. . . . . . . 8
52		incom 3538	. . . . . . . . 9
53		f1dm 5605	. . . . . . . . . . . 12 $\$ $\$ $\$
54	53	adantl 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
55	54	ineq1d 3546	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
56	55, 16	syl6eq 2486	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$ $\$
57	52, 56	syl5eq 2482	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\$ $\$
58	51, 57	syl5eq 2482	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\$ $\$
59		relres 5133	. . . . . . . 8
60		reldm0 5052	. . . . . . . 8
61	59, 60	ax-mp 5	. . . . . . 7
62	58, 61	sylibr 212	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\$ $\$
63		residm 5136	. . . . . . 7
64	63	a1i 11	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\$ $\$
65	62, 64	uneq12d 3506	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\$ $\$
66		uncom 3495	. . . . . 6
67		un0 3657	. . . . . 6
68	66, 67	eqtri 2458	. . . . 5
69	65, 68	syl6eq 2486	. . . 4 $/\$ $/\$ $/\$ $/\$ $\$ $\$
70	50, 69	syl5eq 2482	. . 3 $/\$ $/\$ $/\$ $/\$ $\$ $\$
71		vex 2970	. . . . 5
72		ovex 6111	. . . . . 6
73		resiexg 6509	. . . . . 6
74	72, 73	ax-mp 5	. . . . 5
75	71, 74	unex 6373	. . . 4
76		f1eq1 5596	. . . . 5
77		reseq1 5099	. . . . . 6
78	77	eqeq1d 2446	. . . . 5
79	76, 78	anbi12d 710	. . . 4 $/\$ $/\$
80	75, 79	spcev 3059	. . 3 $/\$ $/\$
81	49, 70, 80	syl2anc 661	. 2 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$
82	9, 81	exlimddv 1692	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1369

wex 1586

wcel 1756

cvv 2967 $\$ cdif 3320

cun 3321

cin 3322

wss 3323

c0 3632

cid 4626

cdm 4835

crn 4836

cres 4837

wrel 4840

wf 5409

wf1 5410

wf1o 5412

cfv 5413 (class class class)co 6086

cfn 7302

c1 9275

cn0 10571

cuz 10853

cfz 11429

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-om 6472 df-1st 6572 df-2nd 6573 df-recs 6824 df-rdg 6858 df-1o 6912 df-oadd 6916 df-er 7093 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-card 8101 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-nn 10315 df-n0 10572 df-z 10639 df-uz 10854 df-fz 11430

This theorem is referenced by: eldioph2b 29054

W3C validator