revccat - Metamath Proof Explorer

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

Theorem revccat 12751

Description: Antiautomorphic property of the reversal operation. (Contributed by Stefan O'Rear, 27-Aug-2015.)

**Assertion**
Ref	Expression
revccat	Word $/\$ Word reverse ++ reverse ++ reverse

Proof of Theorem revccat Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ccatcl 12601	. . . 4 Word $/\$ Word ++ Word
2		revcl 12746	. . . 4 ++ Word reverse ++ Word
3		wrdf 12557	. . . 4 reverse ++ Word reverse ++ ..^reverse ++
4		ffn 5737	. . . 4 reverse ++ ..^reverse ++ reverse ++ ..^reverse ++
5	1, 2, 3, 4	4syl 21	. . 3 Word $/\$ Word reverse ++ ..^reverse ++
6		revlen 12747	. . . . . . 7 ++ Word reverse ++ ++
7	1, 6	syl 16	. . . . . 6 Word $/\$ Word reverse ++ ++
8		ccatlen 12602	. . . . . . 7 Word $/\$ Word ++
9		lencl 12568	. . . . . . . . 9 Word
10	9	nn0cnd 10875	. . . . . . . 8 Word
11		lencl 12568	. . . . . . . . 9 Word
12	11	nn0cnd 10875	. . . . . . . 8 Word
13		addcom 9783	. . . . . . . 8 $/\$
14	10, 12, 13	syl2an 477	. . . . . . 7 Word $/\$ Word
15	8, 14	eqtrd 2498	. . . . . 6 Word $/\$ Word ++
16	7, 15	eqtrd 2498	. . . . 5 Word $/\$ Word reverse ++
17	16	oveq2d 6312	. . . 4 Word $/\$ Word ..^reverse ++ ..^
18	17	fneq2d 5678	. . 3 Word $/\$ Word reverse ++ ..^reverse ++ reverse ++ ..^
19	5, 18	mpbid 210	. 2 Word $/\$ Word reverse ++ ..^
20		revcl 12746	. . . . 5 Word reverse Word
21		revcl 12746	. . . . 5 Word reverse Word
22		ccatcl 12601	. . . . 5 reverse Word $/\$ reverse Word reverse ++ reverse Word
23	20, 21, 22	syl2anr 478	. . . 4 Word $/\$ Word reverse ++ reverse Word
24		wrdf 12557	. . . 4 reverse ++ reverse Word reverse ++ reverse..^reverse ++ reverse
25		ffn 5737	. . . 4 reverse ++ reverse..^reverse ++ reverse reverse ++ reverse ..^reverse ++ reverse
26	23, 24, 25	3syl 20	. . 3 Word $/\$ Word reverse ++ reverse ..^reverse ++ reverse
27		ccatlen 12602	. . . . . . 7 reverse Word $/\$ reverse Word reverse ++ reverse reverse reverse
28	20, 21, 27	syl2anr 478	. . . . . 6 Word $/\$ Word reverse ++ reverse reverse reverse
29		revlen 12747	. . . . . . 7 Word reverse
30		revlen 12747	. . . . . . 7 Word reverse
31	29, 30	oveqan12rd 6316	. . . . . 6 Word $/\$ Word reverse reverse
32	28, 31	eqtrd 2498	. . . . 5 Word $/\$ Word reverse ++ reverse
33	32	oveq2d 6312	. . . 4 Word $/\$ Word ..^reverse ++ reverse ..^
34	33	fneq2d 5678	. . 3 Word $/\$ Word reverse ++ reverse ..^reverse ++ reverse reverse ++ reverse ..^
35	26, 34	mpbid 210	. 2 Word $/\$ Word reverse ++ reverse ..^
36		id 22	. . . 4 ..^ ..^
37	11	nn0zd 10988	. . . . 5 Word
38	37	adantl 466	. . . 4 Word $/\$ Word
39		fzospliti 11855	. . . 4 ..^ $/\$ ..^ $\/$ ..^
40	36, 38, 39	syl2anr 478	. . 3 Word $/\$ Word $/\$ ..^ ..^ $\/$ ..^
41		simpll 753	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
42		simplr 755	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
43		fzoval 11826	. . . . . . . . . . . 12 ..^
44	38, 43	syl 16	. . . . . . . . . . 11 Word $/\$ Word ..^
45	44	eleq2d 2527	. . . . . . . . . 10 Word $/\$ Word ..^
46	45	biimpa 484	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
47		fznn0sub2 11806	. . . . . . . . 9
48	46, 47	syl 16	. . . . . . . 8 Word $/\$ Word $/\$ ..^
49	44	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
50	48, 49	eleqtrrd 2548	. . . . . . 7 Word $/\$ Word $/\$ ..^ ..^
51		ccatval3 12605	. . . . . . 7 Word $/\$ Word $/\$ ..^ ++
52	41, 42, 50, 51	syl3anc 1228	. . . . . 6 Word $/\$ Word $/\$ ..^ ++
53	15	oveq1d 6311	. . . . . . . . . . 11 Word $/\$ Word ++
54	12	adantl 466	. . . . . . . . . . . 12 Word $/\$ Word
55	10	adantr 465	. . . . . . . . . . . 12 Word $/\$ Word
56		1cnd 9629	. . . . . . . . . . . 12 Word $/\$ Word
57	54, 55, 56	addsubd 9971	. . . . . . . . . . 11 Word $/\$ Word
58	53, 57	eqtrd 2498	. . . . . . . . . 10 Word $/\$ Word ++
59	58	oveq1d 6311	. . . . . . . . 9 Word $/\$ Word ++
60	59	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ++
61		peano2zm 10928	. . . . . . . . . . . 12
62	37, 61	syl 16	. . . . . . . . . . 11 Word
63	62	zcnd 10991	. . . . . . . . . 10 Word
64	63	ad2antlr 726	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
65	10	ad2antrr 725	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
66		elfzoelz 11825	. . . . . . . . . . 11 ..^
67	66	zcnd 10991	. . . . . . . . . 10 ..^
68	67	adantl 466	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
69	64, 65, 68	addsubd 9971	. . . . . . . 8 Word $/\$ Word $/\$ ..^
70	60, 69	eqtrd 2498	. . . . . . 7 Word $/\$ Word $/\$ ..^ ++
71	70	fveq2d 5876	. . . . . 6 Word $/\$ Word $/\$ ..^ ++ ++ ++
72		revfv 12748	. . . . . . 7 Word $/\$ ..^ reverse
73	72	adantll 713	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse
74	52, 71, 73	3eqtr4d 2508	. . . . 5 Word $/\$ Word $/\$ ..^ ++ ++ reverse
75	1	adantr 465	. . . . . 6 Word $/\$ Word $/\$ ..^ ++ Word
76		uzid 11120	. . . . . . . . . . 11
77	38, 76	syl 16	. . . . . . . . . 10 Word $/\$ Word
78	9	adantr 465	. . . . . . . . . 10 Word $/\$ Word
79		uzaddcl 11162	. . . . . . . . . 10 $/\$
80	77, 78, 79	syl2anc 661	. . . . . . . . 9 Word $/\$ Word
81	15, 80	eqeltrd 2545	. . . . . . . 8 Word $/\$ Word ++
82		fzoss2 11851	. . . . . . . 8 ++ ..^ ..^ ++
83	81, 82	syl 16	. . . . . . 7 Word $/\$ Word ..^ ..^ ++
84	83	sselda 3499	. . . . . 6 Word $/\$ Word $/\$ ..^ ..^ ++
85		revfv 12748	. . . . . 6 ++ Word $/\$ ..^ ++ reverse ++ ++ ++
86	75, 84, 85	syl2anc 661	. . . . 5 Word $/\$ Word $/\$ ..^ reverse ++ ++ ++
87	20	ad2antlr 726	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse Word
88	21	ad2antrr 725	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse Word
89	29	adantl 466	. . . . . . . . 9 Word $/\$ Word reverse
90	89	oveq2d 6312	. . . . . . . 8 Word $/\$ Word ..^reverse ..^
91	90	eleq2d 2527	. . . . . . 7 Word $/\$ Word ..^reverse ..^
92	91	biimpar 485	. . . . . 6 Word $/\$ Word $/\$ ..^ ..^reverse
93		ccatval1 12603	. . . . . 6 reverse Word $/\$ reverse Word $/\$ ..^reverse reverse ++ reverse reverse
94	87, 88, 92, 93	syl3anc 1228	. . . . 5 Word $/\$ Word $/\$ ..^ reverse ++ reverse reverse
95	74, 86, 94	3eqtr4d 2508	. . . 4 Word $/\$ Word $/\$ ..^ reverse ++ reverse ++ reverse
96	8	oveq1d 6311	. . . . . . . . . . . 12 Word $/\$ Word ++
97	55, 54, 56	addsubd 9971	. . . . . . . . . . . 12 Word $/\$ Word
98	96, 97	eqtrd 2498	. . . . . . . . . . 11 Word $/\$ Word ++
99	98	oveq1d 6311	. . . . . . . . . 10 Word $/\$ Word ++
100	99	adantr 465	. . . . . . . . 9 Word $/\$ Word $/\$ ..^ ++
101	9	nn0zd 10988	. . . . . . . . . . . . 13 Word
102		peano2zm 10928	. . . . . . . . . . . . 13
103	101, 102	syl 16	. . . . . . . . . . . 12 Word
104	103	zcnd 10991	. . . . . . . . . . 11 Word
105	104	ad2antrr 725	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
106		elfzoelz 11825	. . . . . . . . . . . 12 ..^
107	106	zcnd 10991	. . . . . . . . . . 11 ..^
108	107	adantl 466	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
109	12	ad2antlr 726	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
110	105, 108, 109	subsub3d 9980	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
111	100, 110	eqtr4d 2501	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ++
112	89	oveq2d 6312	. . . . . . . . . 10 Word $/\$ Word reverse
113	112	oveq2d 6312	. . . . . . . . 9 Word $/\$ Word reverse
114	113	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ reverse
115	111, 114	eqtr4d 2501	. . . . . . 7 Word $/\$ Word $/\$ ..^ ++ reverse
116	115	fveq2d 5876	. . . . . 6 Word $/\$ Word $/\$ ..^ ++ reverse
117		simpll 753	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
118		simplr 755	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
119		zaddcl 10925	. . . . . . . . . . . 12 $/\$
120	37, 101, 119	syl2anr 478	. . . . . . . . . . 11 Word $/\$ Word
121		peano2zm 10928	. . . . . . . . . . 11
122	120, 121	syl 16	. . . . . . . . . 10 Word $/\$ Word
123	122	adantr 465	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
124		fzoval 11826	. . . . . . . . . . . 12 ..^
125	120, 124	syl 16	. . . . . . . . . . 11 Word $/\$ Word ..^
126	125	eleq2d 2527	. . . . . . . . . 10 Word $/\$ Word ..^
127	126	biimpa 484	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
128		fzrev2i 11769	. . . . . . . . 9 $/\$
129	123, 127, 128	syl2anc 661	. . . . . . . 8 Word $/\$ Word $/\$ ..^
130	53	oveq1d 6311	. . . . . . . . 9 Word $/\$ Word ++
131	130	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ++
132	101	adantr 465	. . . . . . . . . . 11 Word $/\$ Word
133		fzoval 11826	. . . . . . . . . . 11 ..^
134	132, 133	syl 16	. . . . . . . . . 10 Word $/\$ Word ..^
135	122	zcnd 10991	. . . . . . . . . . . 12 Word $/\$ Word
136	135	subidd 9938	. . . . . . . . . . 11 Word $/\$ Word
137		addcl 9591	. . . . . . . . . . . . . 14 $/\$
138	12, 10, 137	syl2anr 478	. . . . . . . . . . . . 13 Word $/\$ Word
139	138, 56, 54	sub32d 9982	. . . . . . . . . . . 12 Word $/\$ Word
140		pncan2 9846	. . . . . . . . . . . . . 14 $/\$
141	12, 10, 140	syl2anr 478	. . . . . . . . . . . . 13 Word $/\$ Word
142	141	oveq1d 6311	. . . . . . . . . . . 12 Word $/\$ Word
143	139, 142	eqtrd 2498	. . . . . . . . . . 11 Word $/\$ Word
144	136, 143	oveq12d 6314	. . . . . . . . . 10 Word $/\$ Word
145	134, 144	eqtr4d 2501	. . . . . . . . 9 Word $/\$ Word ..^
146	145	adantr 465	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
147	129, 131, 146	3eltr4d 2560	. . . . . . 7 Word $/\$ Word $/\$ ..^ ++ ..^
148		ccatval1 12603	. . . . . . 7 Word $/\$ Word $/\$ ++ ..^ ++ ++ ++
149	117, 118, 147, 148	syl3anc 1228	. . . . . 6 Word $/\$ Word $/\$ ..^ ++ ++ ++
150	29	ad2antlr 726	. . . . . . . . 9 Word $/\$ Word $/\$ ..^ reverse
151	150	oveq2d 6312	. . . . . . . 8 Word $/\$ Word $/\$ ..^ reverse
152		id 22	. . . . . . . . 9 ..^ ..^
153		fzosubel3 11879	. . . . . . . . 9 ..^ $/\$ ..^
154	152, 132, 153	syl2anr 478	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
155	151, 154	eqeltrd 2545	. . . . . . 7 Word $/\$ Word $/\$ ..^ reverse ..^
156		revfv 12748	. . . . . . 7 Word $/\$ reverse ..^ reverse reverse reverse
157	117, 155, 156	syl2anc 661	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse reverse reverse
158	116, 149, 157	3eqtr4d 2508	. . . . 5 Word $/\$ Word $/\$ ..^ ++ ++ reverse reverse
159	1	adantr 465	. . . . . 6 Word $/\$ Word $/\$ ..^ ++ Word
160	11	adantl 466	. . . . . . . . 9 Word $/\$ Word
161		fzoss1 11850	. . . . . . . . . 10 ..^ ..^
162		nn0uz 11140	. . . . . . . . . 10
163	161, 162	eleq2s 2565	. . . . . . . . 9 ..^ ..^
164	160, 163	syl 16	. . . . . . . 8 Word $/\$ Word ..^ ..^
165	15	oveq2d 6312	. . . . . . . 8 Word $/\$ Word ..^ ++ ..^
166	164, 165	sseqtr4d 3536	. . . . . . 7 Word $/\$ Word ..^ ..^ ++
167	166	sselda 3499	. . . . . 6 Word $/\$ Word $/\$ ..^ ..^ ++
168	159, 167, 85	syl2anc 661	. . . . 5 Word $/\$ Word $/\$ ..^ reverse ++ ++ ++
169	20	ad2antlr 726	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse Word
170	21	ad2antrr 725	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse Word
171	89, 31	oveq12d 6314	. . . . . . . 8 Word $/\$ Word reverse..^reverse reverse ..^
172	171	eleq2d 2527	. . . . . . 7 Word $/\$ Word reverse..^reverse reverse ..^
173	172	biimpar 485	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse..^reverse reverse
174		ccatval2 12604	. . . . . 6 reverse Word $/\$ reverse Word $/\$ reverse..^reverse reverse reverse ++ reverse reverse reverse
175	169, 170, 173, 174	syl3anc 1228	. . . . 5 Word $/\$ Word $/\$ ..^ reverse ++ reverse reverse reverse
176	158, 168, 175	3eqtr4d 2508	. . . 4 Word $/\$ Word $/\$ ..^ reverse ++ reverse ++ reverse
177	95, 176	jaodan 785	. . 3 Word $/\$ Word $/\$ ..^ $\/$ ..^ reverse ++ reverse ++ reverse
178	40, 177	syldan 470	. 2 Word $/\$ Word $/\$ ..^ reverse ++ reverse ++ reverse
179	19, 35, 178	eqfnfvd 5985	1 Word $/\$ Word reverse ++ reverse ++ reverse

Colors of variables: wff setvar class

Syntax hints:

wi 4 $\/$ wo 368 $/\$ wa 369

wceq 1395

wcel 1819

wss 3471

wfn 5589

wf 5590

cfv 5594 (class class class)co 6296

cc 9507

cc0 9509

c1 9510

caddc 9512

cmin 9824

cn0 10816

cz 10885

cuz 11106

cfz 11697 ..^cfzo 11820

chash 12407 Word cword 12537 ++ cconcat 12539 reversecreverse 12543

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-oadd 7152 df-er 7329 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-card 8337 df-cda 8565 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-nn 10557 df-2 10615 df-n0 10817 df-z 10886 df-uz 11107 df-fz 11698 df-fzo 11821 df-hash 12408 df-word 12545 df-concat 12547 df-reverse 12551

This theorem is referenced by: gsumwrev 16527 efginvrel2 16871

W3C validator