revccat - Metamath Proof Explorer

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

Theorem revccat 13515

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 13359	. . . 4 Word $/\$ Word ++ Word
2		revcl 13510	. . . 4 ++ Word reverse ++ Word
3		wrdf 13310	. . . 4 reverse ++ Word reverse ++ ..^reverse ++
4		ffn 6045	. . . 4 reverse ++ ..^reverse ++ reverse ++ ..^reverse ++
5	1, 2, 3, 4	4syl 19	. . 3 Word $/\$ Word reverse ++ ..^reverse ++
6		revlen 13511	. . . . . . 7 ++ Word reverse ++ ++
7	1, 6	syl 17	. . . . . 6 Word $/\$ Word reverse ++ ++
8		ccatlen 13360	. . . . . . 7 Word $/\$ Word ++
9		lencl 13324	. . . . . . . . 9 Word
10	9	nn0cnd 11353	. . . . . . . 8 Word
11		lencl 13324	. . . . . . . . 9 Word
12	11	nn0cnd 11353	. . . . . . . 8 Word
13		addcom 10222	. . . . . . . 8 $/\$
14	10, 12, 13	syl2an 494	. . . . . . 7 Word $/\$ Word
15	8, 14	eqtrd 2656	. . . . . 6 Word $/\$ Word ++
16	7, 15	eqtrd 2656	. . . . 5 Word $/\$ Word reverse ++
17	16	oveq2d 6666	. . . 4 Word $/\$ Word ..^reverse ++ ..^
18	17	fneq2d 5982	. . 3 Word $/\$ Word reverse ++ ..^reverse ++ reverse ++ ..^
19	5, 18	mpbid 222	. 2 Word $/\$ Word reverse ++ ..^
20		revcl 13510	. . . . 5 Word reverse Word
21		revcl 13510	. . . . 5 Word reverse Word
22		ccatcl 13359	. . . . 5 reverse Word $/\$ reverse Word reverse ++ reverse Word
23	20, 21, 22	syl2anr 495	. . . 4 Word $/\$ Word reverse ++ reverse Word
24		wrdf 13310	. . . 4 reverse ++ reverse Word reverse ++ reverse..^reverse ++ reverse
25		ffn 6045	. . . 4 reverse ++ reverse..^reverse ++ reverse reverse ++ reverse ..^reverse ++ reverse
26	23, 24, 25	3syl 18	. . 3 Word $/\$ Word reverse ++ reverse ..^reverse ++ reverse
27		ccatlen 13360	. . . . . . 7 reverse Word $/\$ reverse Word reverse ++ reverse reverse reverse
28	20, 21, 27	syl2anr 495	. . . . . 6 Word $/\$ Word reverse ++ reverse reverse reverse
29		revlen 13511	. . . . . . 7 Word reverse
30		revlen 13511	. . . . . . 7 Word reverse
31	29, 30	oveqan12rd 6670	. . . . . 6 Word $/\$ Word reverse reverse
32	28, 31	eqtrd 2656	. . . . 5 Word $/\$ Word reverse ++ reverse
33	32	oveq2d 6666	. . . 4 Word $/\$ Word ..^reverse ++ reverse ..^
34	33	fneq2d 5982	. . 3 Word $/\$ Word reverse ++ reverse ..^reverse ++ reverse reverse ++ reverse ..^
35	26, 34	mpbid 222	. 2 Word $/\$ Word reverse ++ reverse ..^
36		id 22	. . . 4 ..^ ..^
37	11	nn0zd 11480	. . . . 5 Word
38	37	adantl 482	. . . 4 Word $/\$ Word
39		fzospliti 12500	. . . 4 ..^ $/\$ ..^ $\/$ ..^
40	36, 38, 39	syl2anr 495	. . 3 Word $/\$ Word $/\$ ..^ ..^ $\/$ ..^
41		simpll 790	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
42		simplr 792	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
43		fzoval 12471	. . . . . . . . . . . 12 ..^
44	38, 43	syl 17	. . . . . . . . . . 11 Word $/\$ Word ..^
45	44	eleq2d 2687	. . . . . . . . . 10 Word $/\$ Word ..^
46	45	biimpa 501	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
47		fznn0sub2 12446	. . . . . . . . 9
48	46, 47	syl 17	. . . . . . . 8 Word $/\$ Word $/\$ ..^
49	44	adantr 481	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
50	48, 49	eleqtrrd 2704	. . . . . . 7 Word $/\$ Word $/\$ ..^ ..^
51		ccatval3 13363	. . . . . . 7 Word $/\$ Word $/\$ ..^ ++
52	41, 42, 50, 51	syl3anc 1326	. . . . . 6 Word $/\$ Word $/\$ ..^ ++
53	15	oveq1d 6665	. . . . . . . . . . 11 Word $/\$ Word ++
54	12	adantl 482	. . . . . . . . . . . 12 Word $/\$ Word
55	10	adantr 481	. . . . . . . . . . . 12 Word $/\$ Word
56		1cnd 10056	. . . . . . . . . . . 12 Word $/\$ Word
57	54, 55, 56	addsubd 10413	. . . . . . . . . . 11 Word $/\$ Word
58	53, 57	eqtrd 2656	. . . . . . . . . 10 Word $/\$ Word ++
59	58	oveq1d 6665	. . . . . . . . 9 Word $/\$ Word ++
60	59	adantr 481	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ++
61		peano2zm 11420	. . . . . . . . . . . 12
62	37, 61	syl 17	. . . . . . . . . . 11 Word
63	62	zcnd 11483	. . . . . . . . . 10 Word
64	63	ad2antlr 763	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
65	10	ad2antrr 762	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
66		elfzoelz 12470	. . . . . . . . . . 11 ..^
67	66	zcnd 11483	. . . . . . . . . 10 ..^
68	67	adantl 482	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
69	64, 65, 68	addsubd 10413	. . . . . . . 8 Word $/\$ Word $/\$ ..^
70	60, 69	eqtrd 2656	. . . . . . 7 Word $/\$ Word $/\$ ..^ ++
71	70	fveq2d 6195	. . . . . 6 Word $/\$ Word $/\$ ..^ ++ ++ ++
72		revfv 13512	. . . . . . 7 Word $/\$ ..^ reverse
73	72	adantll 750	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse
74	52, 71, 73	3eqtr4d 2666	. . . . 5 Word $/\$ Word $/\$ ..^ ++ ++ reverse
75	1	adantr 481	. . . . . 6 Word $/\$ Word $/\$ ..^ ++ Word
76		uzid 11702	. . . . . . . . . . 11
77	38, 76	syl 17	. . . . . . . . . 10 Word $/\$ Word
78	9	adantr 481	. . . . . . . . . 10 Word $/\$ Word
79		uzaddcl 11744	. . . . . . . . . 10 $/\$
80	77, 78, 79	syl2anc 693	. . . . . . . . 9 Word $/\$ Word
81	15, 80	eqeltrd 2701	. . . . . . . 8 Word $/\$ Word ++
82		fzoss2 12496	. . . . . . . 8 ++ ..^ ..^ ++
83	81, 82	syl 17	. . . . . . 7 Word $/\$ Word ..^ ..^ ++
84	83	sselda 3603	. . . . . 6 Word $/\$ Word $/\$ ..^ ..^ ++
85		revfv 13512	. . . . . 6 ++ Word $/\$ ..^ ++ reverse ++ ++ ++
86	75, 84, 85	syl2anc 693	. . . . 5 Word $/\$ Word $/\$ ..^ reverse ++ ++ ++
87	20	ad2antlr 763	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse Word
88	21	ad2antrr 762	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse Word
89	29	adantl 482	. . . . . . . . 9 Word $/\$ Word reverse
90	89	oveq2d 6666	. . . . . . . 8 Word $/\$ Word ..^reverse ..^
91	90	eleq2d 2687	. . . . . . 7 Word $/\$ Word ..^reverse ..^
92	91	biimpar 502	. . . . . 6 Word $/\$ Word $/\$ ..^ ..^reverse
93		ccatval1 13361	. . . . . 6 reverse Word $/\$ reverse Word $/\$ ..^reverse reverse ++ reverse reverse
94	87, 88, 92, 93	syl3anc 1326	. . . . 5 Word $/\$ Word $/\$ ..^ reverse ++ reverse reverse
95	74, 86, 94	3eqtr4d 2666	. . . 4 Word $/\$ Word $/\$ ..^ reverse ++ reverse ++ reverse
96	8	oveq1d 6665	. . . . . . . . . . . 12 Word $/\$ Word ++
97	55, 54, 56	addsubd 10413	. . . . . . . . . . . 12 Word $/\$ Word
98	96, 97	eqtrd 2656	. . . . . . . . . . 11 Word $/\$ Word ++
99	98	oveq1d 6665	. . . . . . . . . 10 Word $/\$ Word ++
100	99	adantr 481	. . . . . . . . 9 Word $/\$ Word $/\$ ..^ ++
101	9	nn0zd 11480	. . . . . . . . . . . . 13 Word
102		peano2zm 11420	. . . . . . . . . . . . 13
103	101, 102	syl 17	. . . . . . . . . . . 12 Word
104	103	zcnd 11483	. . . . . . . . . . 11 Word
105	104	ad2antrr 762	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
106		elfzoelz 12470	. . . . . . . . . . . 12 ..^
107	106	zcnd 11483	. . . . . . . . . . 11 ..^
108	107	adantl 482	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
109	12	ad2antlr 763	. . . . . . . . . 10 Word $/\$ Word $/\$ ..^
110	105, 108, 109	subsub3d 10422	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
111	100, 110	eqtr4d 2659	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ++
112	89	oveq2d 6666	. . . . . . . . . 10 Word $/\$ Word reverse
113	112	oveq2d 6666	. . . . . . . . 9 Word $/\$ Word reverse
114	113	adantr 481	. . . . . . . 8 Word $/\$ Word $/\$ ..^ reverse
115	111, 114	eqtr4d 2659	. . . . . . 7 Word $/\$ Word $/\$ ..^ ++ reverse
116	115	fveq2d 6195	. . . . . 6 Word $/\$ Word $/\$ ..^ ++ reverse
117		simpll 790	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
118		simplr 792	. . . . . . 7 Word $/\$ Word $/\$ ..^ Word
119		zaddcl 11417	. . . . . . . . . . . 12 $/\$
120	37, 101, 119	syl2anr 495	. . . . . . . . . . 11 Word $/\$ Word
121		peano2zm 11420	. . . . . . . . . . 11
122	120, 121	syl 17	. . . . . . . . . 10 Word $/\$ Word
123	122	adantr 481	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
124		fzoval 12471	. . . . . . . . . . . 12 ..^
125	120, 124	syl 17	. . . . . . . . . . 11 Word $/\$ Word ..^
126	125	eleq2d 2687	. . . . . . . . . 10 Word $/\$ Word ..^
127	126	biimpa 501	. . . . . . . . 9 Word $/\$ Word $/\$ ..^
128		fzrev2i 12405	. . . . . . . . 9 $/\$
129	123, 127, 128	syl2anc 693	. . . . . . . 8 Word $/\$ Word $/\$ ..^
130	53	oveq1d 6665	. . . . . . . . 9 Word $/\$ Word ++
131	130	adantr 481	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ++
132	101	adantr 481	. . . . . . . . . . 11 Word $/\$ Word
133		fzoval 12471	. . . . . . . . . . 11 ..^
134	132, 133	syl 17	. . . . . . . . . 10 Word $/\$ Word ..^
135	122	zcnd 11483	. . . . . . . . . . . 12 Word $/\$ Word
136	135	subidd 10380	. . . . . . . . . . 11 Word $/\$ Word
137		addcl 10018	. . . . . . . . . . . . . 14 $/\$
138	12, 10, 137	syl2anr 495	. . . . . . . . . . . . 13 Word $/\$ Word
139	138, 56, 54	sub32d 10424	. . . . . . . . . . . 12 Word $/\$ Word
140		pncan2 10288	. . . . . . . . . . . . . 14 $/\$
141	12, 10, 140	syl2anr 495	. . . . . . . . . . . . 13 Word $/\$ Word
142	141	oveq1d 6665	. . . . . . . . . . . 12 Word $/\$ Word
143	139, 142	eqtrd 2656	. . . . . . . . . . 11 Word $/\$ Word
144	136, 143	oveq12d 6668	. . . . . . . . . 10 Word $/\$ Word
145	134, 144	eqtr4d 2659	. . . . . . . . 9 Word $/\$ Word ..^
146	145	adantr 481	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
147	129, 131, 146	3eltr4d 2716	. . . . . . 7 Word $/\$ Word $/\$ ..^ ++ ..^
148		ccatval1 13361	. . . . . . 7 Word $/\$ Word $/\$ ++ ..^ ++ ++ ++
149	117, 118, 147, 148	syl3anc 1326	. . . . . 6 Word $/\$ Word $/\$ ..^ ++ ++ ++
150	29	ad2antlr 763	. . . . . . . . 9 Word $/\$ Word $/\$ ..^ reverse
151	150	oveq2d 6666	. . . . . . . 8 Word $/\$ Word $/\$ ..^ reverse
152		id 22	. . . . . . . . 9 ..^ ..^
153		fzosubel3 12528	. . . . . . . . 9 ..^ $/\$ ..^
154	152, 132, 153	syl2anr 495	. . . . . . . 8 Word $/\$ Word $/\$ ..^ ..^
155	151, 154	eqeltrd 2701	. . . . . . 7 Word $/\$ Word $/\$ ..^ reverse ..^
156		revfv 13512	. . . . . . 7 Word $/\$ reverse ..^ reverse reverse reverse
157	117, 155, 156	syl2anc 693	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse reverse reverse
158	116, 149, 157	3eqtr4d 2666	. . . . 5 Word $/\$ Word $/\$ ..^ ++ ++ reverse reverse
159	1	adantr 481	. . . . . 6 Word $/\$ Word $/\$ ..^ ++ Word
160	11	adantl 482	. . . . . . . . 9 Word $/\$ Word
161		fzoss1 12495	. . . . . . . . . 10 ..^ ..^
162		nn0uz 11722	. . . . . . . . . 10
163	161, 162	eleq2s 2719	. . . . . . . . 9 ..^ ..^
164	160, 163	syl 17	. . . . . . . 8 Word $/\$ Word ..^ ..^
165	15	oveq2d 6666	. . . . . . . 8 Word $/\$ Word ..^ ++ ..^
166	164, 165	sseqtr4d 3642	. . . . . . 7 Word $/\$ Word ..^ ..^ ++
167	166	sselda 3603	. . . . . 6 Word $/\$ Word $/\$ ..^ ..^ ++
168	159, 167, 85	syl2anc 693	. . . . 5 Word $/\$ Word $/\$ ..^ reverse ++ ++ ++
169	20	ad2antlr 763	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse Word
170	21	ad2antrr 762	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse Word
171	89, 31	oveq12d 6668	. . . . . . . 8 Word $/\$ Word reverse..^reverse reverse ..^
172	171	eleq2d 2687	. . . . . . 7 Word $/\$ Word reverse..^reverse reverse ..^
173	172	biimpar 502	. . . . . 6 Word $/\$ Word $/\$ ..^ reverse..^reverse reverse
174		ccatval2 13362	. . . . . 6 reverse Word $/\$ reverse Word $/\$ reverse..^reverse reverse reverse ++ reverse reverse reverse
175	169, 170, 173, 174	syl3anc 1326	. . . . 5 Word $/\$ Word $/\$ ..^ reverse ++ reverse reverse reverse
176	158, 168, 175	3eqtr4d 2666	. . . 4 Word $/\$ Word $/\$ ..^ reverse ++ reverse ++ reverse
177	95, 176	jaodan 826	. . 3 Word $/\$ Word $/\$ ..^ $\/$ ..^ reverse ++ reverse ++ reverse
178	40, 177	syldan 487	. 2 Word $/\$ Word $/\$ ..^ reverse ++ reverse ++ reverse
179	19, 35, 178	eqfnfvd 6314	1 Word $/\$ Word reverse ++ reverse ++ reverse

Colors of variables: wff setvar class

Syntax hints:

wi 4 $\/$ wo 383 $/\$ wa 384

wceq 1483

wcel 1990

wss 3574

wfn 5883

wf 5884

cfv 5888 (class class class)co 6650

cc 9934

cc0 9936

c1 9937

caddc 9939

cmin 10266

cn0 11292

cz 11377

cuz 11687

cfz 12326 ..^cfzo 12465

chash 13117 Word cword 13291 ++ cconcat 13293 reversecreverse 13297

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327 df-fzo 12466 df-hash 13118 df-word 13299 df-concat 13301 df-reverse 13305

This theorem is referenced by: gsumwrev 17796 efginvrel2 18140

W3C validator