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 30298

Description: Lemma for eldioph2 30299. 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 12046	. . . 4
3		difinf 7786	. . . 4 $/\$ $\$
4	1, 2, 3	sylancl 662	. . 3 $/\$ $/\$ $/\$ $\$
5		fzfi 12046	. . . 4
6		diffi 7747	. . . 4 $\$
7	5, 6	ax-mp 5	. . 3 $\$
8		isinffi 8369	. . 3 $\$ $/\$ $\$ $\$ $\$
9	4, 7, 8	sylancl 662	. 2 $/\$ $/\$ $/\$ $\$ $\$
10		f1f1orn 5825	. . . . . . . 8 $\$ $\$ $\$
11	10	adantl 466	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
12		f1oi 5849	. . . . . . . 8
13	12	a1i 11	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\$ $\$
14		incom 3691	. . . . . . . . 9 $\$ $\$
15		disjdif 3899	. . . . . . . . 9 $\$
16	14, 15	eqtri 2496	. . . . . . . 8 $\$
17	16	a1i 11	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
18		f1f 5779	. . . . . . . . . . . 12 $\$ $\$ $\$ $\$
19		frn 5735	. . . . . . . . . . . 12 $\$ $\$ $\$
20	18, 19	syl 16	. . . . . . . . . . 11 $\$ $\$ $\$
21	20	adantl 466	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
22		ssrin 3723	. . . . . . . . . 10 $\$ $\$
23	21, 22	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
24		incom 3691	. . . . . . . . . 10 $\$ $\$
25		disjdif 3899	. . . . . . . . . 10 $\$
26	24, 25	eqtri 2496	. . . . . . . . 9 $\$
27	23, 26	syl6sseq 3550	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\$ $\$
28		ss0 3816	. . . . . . . 8
29	27, 28	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\$ $\$
30		f1oun 5833	. . . . . . 7 $\$ $/\$ $/\$ $\$ $/\$ $\$
31	11, 13, 17, 29, 30	syl22anc 1229	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
32		f1of1 5813	. . . . . 6 $\$ $\$
33	31, 32	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
34		uncom 3648	. . . . . . 7 $\$ $\$
35		simplrr 760	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$ $\$
36		fzss2 11719	. . . . . . . . 9
37	35, 36	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\$ $\$
38		undif 3907	. . . . . . . 8 $\$
39	37, 38	sylib 196	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
40	34, 39	syl5eq 2520	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
41		f1eq2 5775	. . . . . 6 $\$ $\$
42	40, 41	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
43	33, 42	mpbid 210	. . . 4 $/\$ $/\$ $/\$ $/\$ $\$ $\$
44	20	difss2d 3634	. . . . . 6 $\$ $\$
45	44	adantl 466	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\$ $\$
46		simplrl 759	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\$ $\$
47	45, 46	unssd 3680	. . . 4 $/\$ $/\$ $/\$ $/\$ $\$ $\$
48		f1ss 5784	. . . 4 $/\$
49	43, 47, 48	syl2anc 661	. . 3 $/\$ $/\$ $/\$ $/\$ $\$ $\$
50		resundir 5286	. . . 4
51		dmres 5292	. . . . . . . 8
52		incom 3691	. . . . . . . . 9
53		f1dm 5783	. . . . . . . . . . . 12 $\$ $\$ $\$
54	53	adantl 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
55	54	ineq1d 3699	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
56	55, 16	syl6eq 2524	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$ $\$
57	52, 56	syl5eq 2520	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\$ $\$
58	51, 57	syl5eq 2520	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\$ $\$
59		relres 5299	. . . . . . . 8
60		reldm0 5218	. . . . . . . 8
61	59, 60	ax-mp 5	. . . . . . 7
62	58, 61	sylibr 212	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\$ $\$
63		residm 5303	. . . . . . 7
64	63	a1i 11	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\$ $\$
65	62, 64	uneq12d 3659	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\$ $\$
66		uncom 3648	. . . . . 6
67		un0 3810	. . . . . 6
68	66, 67	eqtri 2496	. . . . 5
69	65, 68	syl6eq 2524	. . . 4 $/\$ $/\$ $/\$ $/\$ $\$ $\$
70	50, 69	syl5eq 2520	. . 3 $/\$ $/\$ $/\$ $/\$ $\$ $\$
71		vex 3116	. . . . 5
72		ovex 6307	. . . . . 6
73		resiexg 6717	. . . . . 6
74	72, 73	ax-mp 5	. . . . 5
75	71, 74	unex 6580	. . . 4
76		f1eq1 5774	. . . . 5
77		reseq1 5265	. . . . . 6
78	77	eqeq1d 2469	. . . . 5
79	76, 78	anbi12d 710	. . . 4 $/\$ $/\$
80	75, 79	spcev 3205	. . 3 $/\$ $/\$
81	49, 70, 80	syl2anc 661	. 2 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$
82	9, 81	exlimddv 1702	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1379

wex 1596

wcel 1767

cvv 3113 $\$ cdif 3473

cun 3474

cin 3475

wss 3476

c0 3785

cid 4790

cdm 4999

crn 5000

cres 5001

wrel 5004

wf 5582

wf1 5583

wf1o 5585

cfv 5586 (class class class)co 6282

cfn 7513

c1 9489

cn0 10791

cuz 11078

cfz 11668

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-om 6679 df-1st 6781 df-2nd 6782 df-recs 7039 df-rdg 7073 df-1o 7127 df-oadd 7131 df-er 7308 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-card 8316 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-nn 10533 df-n0 10792 df-z 10861 df-uz 11079 df-fz 11669

This theorem is referenced by: eldioph2b 30300

W3C validator