injresinjlem - Metamath Proof Explorer

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

Theorem injresinjlem 11154

Description: Lemma for injresinj 11155. (Contributed by Alexander van der Vekens, 31-Oct-2017.)

**Assertion**
Ref	Expression
injresinjlem	..^ $/\$ ..^ $/\$

Proof of Theorem injresinjlem Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfznelfzo 11147	. . . . . . 7 $/\$ ..^ $\/$
2		ffn 5550	. . . . . . . . . . . . . . . . . 18
3	2	adantr 452	. . . . . . . . . . . . . . . . 17 $/\$
4		0nn0 10192	. . . . . . . . . . . . . . . . . . . 20
5	4	a1i 11	. . . . . . . . . . . . . . . . . . 19
6		id 20	. . . . . . . . . . . . . . . . . . 19
7		nn0ge0 10203	. . . . . . . . . . . . . . . . . . 19
8		elfz2nn0 11038	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
9	5, 6, 7, 8	syl3anbrc 1138	. . . . . . . . . . . . . . . . . 18
10	9	adantl 453	. . . . . . . . . . . . . . . . 17 $/\$
11		nn0re 10186	. . . . . . . . . . . . . . . . . . . 20
12	11	leidd 9549	. . . . . . . . . . . . . . . . . . 19
13		elfz2nn0 11038	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
14	6, 6, 12, 13	syl3anbrc 1138	. . . . . . . . . . . . . . . . . 18
15	14	adantl 453	. . . . . . . . . . . . . . . . 17 $/\$
16		fnimapr 5746	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
17	3, 10, 15, 16	syl3anc 1184	. . . . . . . . . . . . . . . 16 $/\$
18	17	ineq1d 3501	. . . . . . . . . . . . . . 15 $/\$ ..^ ..^
19	18	eqeq1d 2412	. . . . . . . . . . . . . 14 $/\$ ..^ ..^
20		disj 3628	. . . . . . . . . . . . . 14 ..^ ..^
21	19, 20	syl6bb 253	. . . . . . . . . . . . 13 $/\$ ..^ ..^
22		fvex 5701	. . . . . . . . . . . . . . . 16
23		fvex 5701	. . . . . . . . . . . . . . . 16
24	22, 23	pm3.2i 442	. . . . . . . . . . . . . . 15 $/\$
25		eleq1 2464	. . . . . . . . . . . . . . . . 17 ..^ ..^
26	25	notbid 286	. . . . . . . . . . . . . . . 16 ..^ ..^
27		eleq1 2464	. . . . . . . . . . . . . . . . 17 ..^ ..^
28	27	notbid 286	. . . . . . . . . . . . . . . 16 ..^ ..^
29	26, 28	ralprg 3817	. . . . . . . . . . . . . . 15 $/\$ ..^ ..^ $/\$ ..^
30	24, 29	mp1i 12	. . . . . . . . . . . . . 14 $/\$ ..^ ..^ $/\$ ..^
31		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . 23
32	31	eqcoms 2407	. . . . . . . . . . . . . . . . . . . . . 22
33	32	eleq1d 2470	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
34	33	notbid 286	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^
35	34	biimpd 199	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
36		1nn0 10193	. . . . . . . . . . . . . . . . . . . . . . . . . 26
37		elnn0uz 10479	. . . . . . . . . . . . . . . . . . . . . . . . . 26
38	36, 37	mpbi 200	. . . . . . . . . . . . . . . . . . . . . . . . 25
39		fzoss1 11117	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
40	38, 39	mp1i 12	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
41		fzossfz 11112	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^
42	40, 41	syl6ss 3320	. . . . . . . . . . . . . . . . . . . . . . 23 ..^
43		fvelimab 5741	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ ..^ ..^
44	2, 42, 43	syl2an 464	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ ..^
45	44	notbid 286	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ ..^
46		ralnex 2676	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
47		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
48	47	eqeq1d 2412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
49	48	notbid 286	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
50	49	rspcva 3010	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ $/\$ ..^
51		pm2.21 102	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
52	51	a1d 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
53	52	a1d 23	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
54	53	a1d 23	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
55	50, 54	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$ ..^ $/\$
56	55	expcom 425	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^ $/\$
57	56	com24 83	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$ ..^
58	46, 57	sylbir 205	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$ ..^
59	58	com12 29	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ ..^
60	45, 59	sylbid 207	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ ..^
61	60	com12 29	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$ ..^
62	35, 61	syl6com 33	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ ..^
63	62	adantr 452	. . . . . . . . . . . . . . . . 17 ..^ $/\$ ..^ $/\$ ..^
64	63	com12 29	. . . . . . . . . . . . . . . 16 ..^ $/\$ ..^ $/\$ ..^
65		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . 23
66	65	eqcoms 2407	. . . . . . . . . . . . . . . . . . . . . 22
67	66	eleq1d 2470	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
68	67	notbid 286	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^
69	68	biimpd 199	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
70	69, 61	syl6com 33	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ ..^
71	70	adantl 453	. . . . . . . . . . . . . . . . 17 ..^ $/\$ ..^ $/\$ ..^
72	71	com12 29	. . . . . . . . . . . . . . . 16 ..^ $/\$ ..^ $/\$ ..^
73	64, 72	jaoi 369	. . . . . . . . . . . . . . 15 $\/$ ..^ $/\$ ..^ $/\$ ..^
74	73	com13 76	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ ..^ $\/$ ..^
75	30, 74	sylbid 207	. . . . . . . . . . . . 13 $/\$ ..^ $\/$ ..^
76	21, 75	sylbid 207	. . . . . . . . . . . 12 $/\$ ..^ $\/$ ..^
77	76	com14 84	. . . . . . . . . . 11 ..^ $\/$ $/\$ ..^
78	77	com12 29	. . . . . . . . . 10 ..^ $\/$ $/\$ ..^
79	78	com15 89	. . . . . . . . 9 ..^ $\/$ $/\$ ..^
80		elfznelfzo 11147	. . . . . . . . . . 11 $/\$ ..^ $\/$
81		eqtr3 2423	. . . . . . . . . . . . . 14 $/\$
82		id 20	. . . . . . . . . . . . . . . . . 18
83	82	a1d 23	. . . . . . . . . . . . . . . . 17
84	83	a1d 23	. . . . . . . . . . . . . . . 16
85	84	a1d 23	. . . . . . . . . . . . . . 15 ..^
86	85	a1d 23	. . . . . . . . . . . . . 14 $/\$ ..^
87	81, 86	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ ..^
88	32	adantl 453	. . . . . . . . . . . . . . . . 17 $/\$
89		fveq2 5687	. . . . . . . . . . . . . . . . . . 19
90	89	eqcoms 2407	. . . . . . . . . . . . . . . . . 18
91	90	adantr 452	. . . . . . . . . . . . . . . . 17 $/\$
92	88, 91	neeq12d 2582	. . . . . . . . . . . . . . . 16 $/\$
93		df-ne 2569	. . . . . . . . . . . . . . . . 17
94		pm2.24 103	. . . . . . . . . . . . . . . . . . 19
95	94	eqcoms 2407	. . . . . . . . . . . . . . . . . 18
96	95	com12 29	. . . . . . . . . . . . . . . . 17
97	93, 96	sylbi 188	. . . . . . . . . . . . . . . 16
98	92, 97	syl6bi 220	. . . . . . . . . . . . . . 15 $/\$
99	98	a1d 23	. . . . . . . . . . . . . 14 $/\$ ..^
100	99	a1d 23	. . . . . . . . . . . . 13 $/\$ $/\$ ..^
101		fveq2 5687	. . . . . . . . . . . . . . . . . . 19
102	101	eqcoms 2407	. . . . . . . . . . . . . . . . . 18
103	102	adantr 452	. . . . . . . . . . . . . . . . 17 $/\$
104	66	adantl 453	. . . . . . . . . . . . . . . . 17 $/\$
105	103, 104	neeq12d 2582	. . . . . . . . . . . . . . . 16 $/\$
106		df-ne 2569	. . . . . . . . . . . . . . . . 17
107	106, 51	sylbi 188	. . . . . . . . . . . . . . . 16
108	105, 107	syl6bi 220	. . . . . . . . . . . . . . 15 $/\$
109	108	a1d 23	. . . . . . . . . . . . . 14 $/\$ ..^
110	109	a1d 23	. . . . . . . . . . . . 13 $/\$ $/\$ ..^
111		eqtr3 2423	. . . . . . . . . . . . . 14 $/\$
112	111, 86	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ ..^
113	87, 100, 110, 112	ccase 913	. . . . . . . . . . . 12 $\/$ $/\$ $\/$ $/\$ ..^
114	113	ex 424	. . . . . . . . . . 11 $\/$ $\/$ $/\$ ..^
115	80, 114	syl 16	. . . . . . . . . 10 $/\$ ..^ $\/$ $/\$ ..^
116	115	expcom 425	. . . . . . . . 9 ..^ $\/$ $/\$ ..^
117	79, 116	pm2.61i 158	. . . . . . . 8 $\/$ $/\$ ..^
118	117	com12 29	. . . . . . 7 $\/$ $/\$ ..^
119	1, 118	syl 16	. . . . . 6 $/\$ ..^ $/\$ ..^
120	119	ex 424	. . . . 5 ..^ $/\$ ..^
121	120	com23 74	. . . 4 ..^ $/\$ ..^
122	121	impcom 420	. . 3 $/\$ ..^ $/\$ ..^
123	122	com12 29	. 2 ..^ $/\$ $/\$ ..^
124	123	com25 87	1 ..^ $/\$ ..^ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $\/$ wo 358 $/\$ wa 359

wceq 1649

wcel 1721

wne 2567

wral 2666

wrex 2667

cvv 2916

cin 3279

wss 3280

c0 3588

cpr 3775 class class class wbr 4172

cima 4840

wfn 5408

wf 5409

cfv 5413 (class class class)co 6040

cc0 8946

c1 8947

cle 9077

cn0 10177

cuz 10444

cfz 10999 ..^cfzo 11090

This theorem is referenced by: injresinj 11155

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-er 6864 df-en 7069 df-dom 7070 df-sdom 7071 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-nn 9957 df-n0 10178 df-z 10239 df-uz 10445 df-fz 11000 df-fzo 11091

W3C validator