splcl - Metamath Proof Explorer

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

Theorem splcl 12866

Description: Closure of the substring replacement operator. (Contributed by Stefan O'Rear, 26-Aug-2015.)

**Assertion**
Ref	Expression
splcl	Word $/\$ Word splice Word

Proof of Theorem splcl Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3056	. . . 4 Word
2		otex 4668	. . . 4
3		id 22	. . . . . . . 8
4		fveq2 5870	. . . . . . . . . 10
5	4	fveq2d 5874	. . . . . . . . 9
6	5	opeq2d 4176	. . . . . . . 8
7	3, 6	oveqan12d 6314	. . . . . . 7 $/\$ substr substr
8		simpr 463	. . . . . . . 8 $/\$
9	8	fveq2d 5874	. . . . . . 7 $/\$
10	7, 9	oveq12d 6313	. . . . . 6 $/\$ substr ++ substr ++
11		simpl 459	. . . . . . 7 $/\$
12	8	fveq2d 5874	. . . . . . . . 9 $/\$
13	12	fveq2d 5874	. . . . . . . 8 $/\$
14	11	fveq2d 5874	. . . . . . . 8 $/\$
15	13, 14	opeq12d 4177	. . . . . . 7 $/\$
16	11, 15	oveq12d 6313	. . . . . 6 $/\$ substr substr
17	10, 16	oveq12d 6313	. . . . 5 $/\$ substr ++ ++ substr substr ++ ++ substr
18		df-splice 12676	. . . . 5 splice substr ++ ++ substr
19		ovex 6323	. . . . 5 substr ++ ++ substr
20	17, 18, 19	ovmpt2a 6432	. . . 4 $/\$ splice substr ++ ++ substr
21	1, 2, 20	sylancl 669	. . 3 Word splice substr ++ ++ substr
22	21	adantr 467	. 2 Word $/\$ Word splice substr ++ ++ substr
23		swrdcl 12782	. . . . 5 Word substr Word
24	23	adantr 467	. . . 4 Word $/\$ Word substr Word
25		ot3rdg 6814	. . . . . 6 Word
26	25	adantl 468	. . . . 5 Word $/\$ Word
27		simpr 463	. . . . 5 Word $/\$ Word Word
28	26, 27	eqeltrd 2531	. . . 4 Word $/\$ Word Word
29		ccatcl 12727	. . . 4 substr Word $/\$ Word substr ++ Word
30	24, 28, 29	syl2anc 667	. . 3 Word $/\$ Word substr ++ Word
31		swrdcl 12782	. . . 4 Word substr Word
32	31	adantr 467	. . 3 Word $/\$ Word substr Word
33		ccatcl 12727	. . 3 substr ++ Word $/\$ substr Word substr ++ ++ substr Word
34	30, 32, 33	syl2anc 667	. 2 Word $/\$ Word substr ++ ++ substr Word
35	22, 34	eqeltrd 2531	1 Word $/\$ Word splice Word

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 371

wceq 1446

wcel 1889

cvv 3047

cop 3976

cotp 3978

cfv 5585 (class class class)co 6295

c1st 6796

c2nd 6797

cc0 9544

chash 12522 Word cword 12663 ++ cconcat 12665 substr csubstr 12667 splice csplice 12668

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-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-ot 3979 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-concat 12673 df-substr 12675 df-splice 12676

This theorem is referenced by: psgnunilem2 17148 efglem 17378 efgtf 17384 frgpuplem 17434

W3C validator