wwlkextinj - Metamath Proof Explorer

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

Theorem wwlkextinj 25470

Description: Lemma 2 for wwlkextbij 25473. (Contributed by Alexander van der Vekens, 7-Aug-2018.)

**Hypotheses**
Ref	Expression
wwlkextbij.d	Word $/\$ substr $/\$ lastS lastS
wwlkextbij.r	lastS
wwlkextbij.f	lastS

**Assertion**
Ref	Expression
wwlkextinj

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

Proof of Theorem wwlkextinj Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wwlkextbij.d	. . 3 Word $/\$ substr $/\$ lastS lastS
2		wwlkextbij.r	. . 3 lastS
3		wwlkextbij.f	. . 3 lastS
4	1, 2, 3	wwlkextfun 25469	. 2
5		fveq2 5870	. . . . . . 7 lastS lastS
6		fvex 5880	. . . . . . 7 lastS
7	5, 3, 6	fvmpt 5953	. . . . . 6 lastS
8		fveq2 5870	. . . . . . 7 lastS lastS
9		fvex 5880	. . . . . . 7 lastS
10	8, 3, 9	fvmpt 5953	. . . . . 6 lastS
11	7, 10	eqeqan12d 2469	. . . . 5 $/\$ lastS lastS
12	11	adantl 468	. . . 4 $/\$ $/\$ lastS lastS
13		fveq2 5870	. . . . . . . . 9
14	13	eqeq1d 2455	. . . . . . . 8
15		oveq1 6302	. . . . . . . . 9 substr substr
16	15	eqeq1d 2455	. . . . . . . 8 substr substr
17		fveq2 5870	. . . . . . . . . 10 lastS lastS
18	17	preq2d 4061	. . . . . . . . 9 lastS lastS lastS lastS
19	18	eleq1d 2515	. . . . . . . 8 lastS lastS lastS lastS
20	14, 16, 19	3anbi123d 1341	. . . . . . 7 $/\$ substr $/\$ lastS lastS $/\$ substr $/\$ lastS lastS
21	20, 1	elrab2 3200	. . . . . 6 Word $/\$ $/\$ substr $/\$ lastS lastS
22		fveq2 5870	. . . . . . . . 9
23	22	eqeq1d 2455	. . . . . . . 8
24		oveq1 6302	. . . . . . . . 9 substr substr
25	24	eqeq1d 2455	. . . . . . . 8 substr substr
26		fveq2 5870	. . . . . . . . . 10 lastS lastS
27	26	preq2d 4061	. . . . . . . . 9 lastS lastS lastS lastS
28	27	eleq1d 2515	. . . . . . . 8 lastS lastS lastS lastS
29	23, 25, 28	3anbi123d 1341	. . . . . . 7 $/\$ substr $/\$ lastS lastS $/\$ substr $/\$ lastS lastS
30	29, 1	elrab2 3200	. . . . . 6 Word $/\$ $/\$ substr $/\$ lastS lastS
31		eqtr3 2474	. . . . . . . . . . . . . . . . 17 $/\$
32	31	expcom 437	. . . . . . . . . . . . . . . 16
33	32	3ad2ant1 1030	. . . . . . . . . . . . . . 15 $/\$ substr $/\$ lastS lastS
34	33	adantl 468	. . . . . . . . . . . . . 14 Word $/\$ $/\$ substr $/\$ lastS lastS
35	34	com12 32	. . . . . . . . . . . . 13 Word $/\$ $/\$ substr $/\$ lastS lastS
36	35	3ad2ant1 1030	. . . . . . . . . . . 12 $/\$ substr $/\$ lastS lastS Word $/\$ $/\$ substr $/\$ lastS lastS
37	36	adantl 468	. . . . . . . . . . 11 Word $/\$ $/\$ substr $/\$ lastS lastS Word $/\$ $/\$ substr $/\$ lastS lastS
38	37	imp 431	. . . . . . . . . 10 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ $/\$ substr $/\$ lastS lastS
39	38	adantr 467	. . . . . . . . 9 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ $/\$ substr $/\$ lastS lastS $/\$
40	39	adantr 467	. . . . . . . 8 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ $/\$ lastS lastS
41		simpr 463	. . . . . . . 8 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ $/\$ lastS lastS lastS lastS
42		eqtr3 2474	. . . . . . . . . . . . . . . . . . . 20 substr $/\$ substr substr substr
43		1e2m1 10732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
44	43	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
45	44	oveq2d 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
46		nn0cn 10886	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
47		2cnd 10689	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
48		1cnd 9664	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
49	46, 47, 48	addsubassd 10011	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
50	45, 49	eqtr4d 2490	. . . . . . . . . . . . . . . . . . . . . . . . . 26
51	50	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
52		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
53	52	eqeq2d 2463	. . . . . . . . . . . . . . . . . . . . . . . . . 26
54	53	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
55	51, 54	mpbird 236	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
56		opeq2 4170	. . . . . . . . . . . . . . . . . . . . . . . . . 26
57	56	oveq2d 6311	. . . . . . . . . . . . . . . . . . . . . . . . 25 substr substr
58	56	oveq2d 6311	. . . . . . . . . . . . . . . . . . . . . . . . 25 substr substr
59	57, 58	eqeq12d 2468	. . . . . . . . . . . . . . . . . . . . . . . 24 substr substr substr substr
60	55, 59	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ substr substr substr substr
61	60	biimpd 211	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ substr substr substr substr
62	61	ex 436	. . . . . . . . . . . . . . . . . . . . 21 substr substr substr substr
63	62	com13 83	. . . . . . . . . . . . . . . . . . . 20 substr substr substr substr
64	42, 63	syl 17	. . . . . . . . . . . . . . . . . . 19 substr $/\$ substr substr substr
65	64	ex 436	. . . . . . . . . . . . . . . . . 18 substr substr substr substr
66	65	com23 81	. . . . . . . . . . . . . . . . 17 substr substr substr substr
67	66	impcom 432	. . . . . . . . . . . . . . . 16 $/\$ substr substr substr substr
68	67	com12 32	. . . . . . . . . . . . . . 15 substr $/\$ substr substr substr
69	68	3ad2ant2 1031	. . . . . . . . . . . . . 14 $/\$ substr $/\$ lastS lastS $/\$ substr substr substr
70	69	adantl 468	. . . . . . . . . . . . 13 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ substr substr substr
71	70	com12 32	. . . . . . . . . . . 12 $/\$ substr Word $/\$ $/\$ substr $/\$ lastS lastS substr substr
72	71	3adant3 1029	. . . . . . . . . . 11 $/\$ substr $/\$ lastS lastS Word $/\$ $/\$ substr $/\$ lastS lastS substr substr
73	72	adantl 468	. . . . . . . . . 10 Word $/\$ $/\$ substr $/\$ lastS lastS Word $/\$ $/\$ substr $/\$ lastS lastS substr substr
74	73	imp31 434	. . . . . . . . 9 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ substr substr
75	74	adantr 467	. . . . . . . 8 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ $/\$ lastS lastS substr substr
76		simpl 459	. . . . . . . . . . . . 13 Word $/\$ $/\$ substr $/\$ lastS lastS Word
77		simpl 459	. . . . . . . . . . . . 13 Word $/\$ $/\$ substr $/\$ lastS lastS Word
78	76, 77	anim12i 570	. . . . . . . . . . . 12 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ $/\$ substr $/\$ lastS lastS Word $/\$ Word
79	78	adantr 467	. . . . . . . . . . 11 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ Word
80		nn0re 10885	. . . . . . . . . . . . . . . . . . . . 21
81		2re 10686	. . . . . . . . . . . . . . . . . . . . . 22
82	81	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
83		nn0ge0 10902	. . . . . . . . . . . . . . . . . . . . 21
84		2pos 10708	. . . . . . . . . . . . . . . . . . . . . 22
85	84	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
86	80, 82, 83, 85	addgegt0d 10194	. . . . . . . . . . . . . . . . . . . 20
87	86	adantl 468	. . . . . . . . . . . . . . . . . . 19 $/\$
88		breq2 4409	. . . . . . . . . . . . . . . . . . . 20
89	88	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$
90	87, 89	mpbird 236	. . . . . . . . . . . . . . . . . 18 $/\$
91		hashgt0n0 12553	. . . . . . . . . . . . . . . . . 18 Word $/\$
92	90, 91	sylan2 477	. . . . . . . . . . . . . . . . 17 Word $/\$ $/\$
93	92	exp32 610	. . . . . . . . . . . . . . . 16 Word
94	93	com12 32	. . . . . . . . . . . . . . 15 Word
95	94	3ad2ant1 1030	. . . . . . . . . . . . . 14 $/\$ substr $/\$ lastS lastS Word
96	95	impcom 432	. . . . . . . . . . . . 13 Word $/\$ $/\$ substr $/\$ lastS lastS
97	96	adantr 467	. . . . . . . . . . . 12 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ $/\$ substr $/\$ lastS lastS
98	97	imp 431	. . . . . . . . . . 11 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ $/\$ substr $/\$ lastS lastS $/\$
99	86	adantl 468	. . . . . . . . . . . . . . . . . . 19 $/\$
100		breq2 4409	. . . . . . . . . . . . . . . . . . . 20
101	100	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$
102	99, 101	mpbird 236	. . . . . . . . . . . . . . . . . 18 $/\$
103		hashgt0n0 12553	. . . . . . . . . . . . . . . . . 18 Word $/\$
104	102, 103	sylan2 477	. . . . . . . . . . . . . . . . 17 Word $/\$ $/\$
105	104	exp32 610	. . . . . . . . . . . . . . . 16 Word
106	105	com12 32	. . . . . . . . . . . . . . 15 Word
107	106	3ad2ant1 1030	. . . . . . . . . . . . . 14 $/\$ substr $/\$ lastS lastS Word
108	107	impcom 432	. . . . . . . . . . . . 13 Word $/\$ $/\$ substr $/\$ lastS lastS
109	108	adantl 468	. . . . . . . . . . . 12 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ $/\$ substr $/\$ lastS lastS
110	109	imp 431	. . . . . . . . . . 11 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ $/\$ substr $/\$ lastS lastS $/\$
111	79, 98, 110	jca32 538	. . . . . . . . . 10 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ Word $/\$ $/\$
112	111	adantr 467	. . . . . . . . 9 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ $/\$ lastS lastS Word $/\$ Word $/\$ $/\$
113		simpl 459	. . . . . . . . . . . 12 Word $/\$ Word Word
114	113	adantr 467	. . . . . . . . . . 11 Word $/\$ Word $/\$ $/\$ Word
115		simpr 463	. . . . . . . . . . . 12 Word $/\$ Word Word
116	115	adantr 467	. . . . . . . . . . 11 Word $/\$ Word $/\$ $/\$ Word
117		hashneq0 12552	. . . . . . . . . . . . . . . 16 Word
118	117	biimprd 227	. . . . . . . . . . . . . . 15 Word
119	118	adantr 467	. . . . . . . . . . . . . 14 Word $/\$ Word
120	119	com12 32	. . . . . . . . . . . . 13 Word $/\$ Word
121	120	adantr 467	. . . . . . . . . . . 12 $/\$ Word $/\$ Word
122	121	impcom 432	. . . . . . . . . . 11 Word $/\$ Word $/\$ $/\$
123		2swrd1eqwrdeq 12817	. . . . . . . . . . 11 Word $/\$ Word $/\$ $/\$ substr substr $/\$ lastS lastS
124	114, 116, 122, 123	syl3anc 1269	. . . . . . . . . 10 Word $/\$ Word $/\$ $/\$ $/\$ substr substr $/\$ lastS lastS
125		ancom 452	. . . . . . . . . . . 12 substr substr $/\$ lastS lastS lastS lastS $/\$ substr substr
126	125	anbi2i 701	. . . . . . . . . . 11 $/\$ substr substr $/\$ lastS lastS $/\$ lastS lastS $/\$ substr substr
127		3anass 990	. . . . . . . . . . 11 $/\$ lastS lastS $/\$ substr substr $/\$ lastS lastS $/\$ substr substr
128	126, 127	bitr4i 256	. . . . . . . . . 10 $/\$ substr substr $/\$ lastS lastS $/\$ lastS lastS $/\$ substr substr
129	124, 128	syl6bb 265	. . . . . . . . 9 Word $/\$ Word $/\$ $/\$ $/\$ lastS lastS $/\$ substr substr
130	112, 129	syl 17	. . . . . . . 8 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ $/\$ lastS lastS $/\$ lastS lastS $/\$ substr substr
131	40, 41, 75, 130	mpbir3and 1192	. . . . . . 7 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ $/\$ lastS lastS
132	131	exp31 609	. . . . . 6 Word $/\$ $/\$ substr $/\$ lastS lastS $/\$ Word $/\$ $/\$ substr $/\$ lastS lastS lastS lastS
133	21, 30, 132	syl2anb 482	. . . . 5 $/\$ lastS lastS
134	133	impcom 432	. . . 4 $/\$ $/\$ lastS lastS
135	12, 134	sylbid 219	. . 3 $/\$ $/\$
136	135	ralrimivva 2811	. 2
137		dff13 6164	. 2 $/\$
138	4, 136, 137	sylanbrc 671	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 986

wceq 1446

wcel 1889

wne 2624

wral 2739

crab 2743

c0 3733

cpr 3972

cop 3976 class class class wbr 4405

cmpt 4464

crn 4838

wf 5581

wf1 5582

cfv 5585 (class class class)co 6295

cr 9543

cc0 9544

c1 9545

caddc 9547

clt 9680

cmin 9865

c2 10666

cn0 10876

chash 12522 Word cword 12663 lastS clsw 12664 substr csubstr 12667

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-rep 4518 ax-sep 4528 ax-nul 4537 ax-pow 4584 ax-pr 4642 ax-un 6588 ax-cnex 9600 ax-resscn 9601 ax-1cn 9602 ax-icn 9603 ax-addcl 9604 ax-addrcl 9605 ax-mulcl 9606 ax-mulrcl 9607 ax-mulcom 9608 ax-addass 9609 ax-mulass 9610 ax-distr 9611 ax-i2m1 9612 ax-1ne0 9613 ax-1rid 9614 ax-rnegex 9615 ax-rrecex 9616 ax-cnre 9617 ax-pre-lttri 9618 ax-pre-lttrn 9619 ax-pre-ltadd 9620 ax-pre-mulgt0 9621

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-fal 1452 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-nel 2627 df-ral 2744 df-rex 2745 df-reu 2746 df-rmo 2747 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-pss 3422 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-tp 3975 df-op 3977 df-uni 4202 df-int 4238 df-iun 4283 df-br 4406 df-opab 4465 df-mpt 4466 df-tr 4501 df-eprel 4748 df-id 4752 df-po 4758 df-so 4759 df-fr 4796 df-we 4798 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-pred 5383 df-ord 5429 df-on 5430 df-lim 5431 df-suc 5432 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593 df-riota 6257 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-om 6698 df-1st 6798 df-2nd 6799 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-1o 7187 df-oadd 7191 df-er 7368 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-card 8378 df-cda 8603 df-pnf 9682 df-mnf 9683 df-xr 9684 df-ltxr 9685 df-le 9686 df-sub 9867 df-neg 9868 df-nn 10617 df-2 10675 df-n0 10877 df-z 10945 df-uz 11167 df-fz 11792 df-fzo 11923 df-hash 12523 df-word 12671 df-lsw 12672 df-s1 12674 df-substr 12675

This theorem is referenced by: wwlkextbij0 25472

W3C validator