cycpmco2f1 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cycpmco2f1		Structured version Visualization version GIF version

Theorem cycpmco2f1 30816

Description: The word U used in cycpmco2 30825 is injective, so it can represent a cycle and form a cyclic permutation (𝑀‘𝑈). (Contributed by Thierry Arnoux, 4-Jan-2024.)

**Hypotheses**
Ref	Expression
cycpmco2.c	⊢ 𝑀 = (toCyc‘𝐷)
cycpmco2.s	⊢ 𝑆 = (SymGrp‘𝐷)
cycpmco2.d	⊢ (𝜑 → 𝐷 ∈ 𝑉)
cycpmco2.w	⊢ (𝜑 → 𝑊 ∈ dom 𝑀)
cycpmco2.i	⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))
cycpmco2.j	⊢ (𝜑 → 𝐽 ∈ ran 𝑊)
cycpmco2.e	⊢ 𝐸 = ((^◡𝑊‘𝐽) + 1)
cycpmco2.1	⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)

**Assertion**
Ref	Expression
cycpmco2f1	⊢ (𝜑 → 𝑈:dom 𝑈–1-1→𝐷)

Proof of Theorem cycpmco2f1 Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cycpmco2.d	. . 3 ⊢ (𝜑 → 𝐷 ∈ 𝑉)
2		ssrab2 4007	. . . . . 6 ⊢ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ⊆ Word 𝐷
3		cycpmco2.w	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)
4		cycpmco2.c	. . . . . . . . . 10 ⊢ 𝑀 = (toCyc‘𝐷)
5		cycpmco2.s	. . . . . . . . . 10 ⊢ 𝑆 = (SymGrp‘𝐷)
6		eqid 2798	. . . . . . . . . 10 ⊢ (Base‘𝑆) = (Base‘𝑆)
7	4, 5, 6	tocycf 30809	. . . . . . . . 9 ⊢ (𝐷 ∈ 𝑉 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆))
8	1, 7	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆))
9	8	fdmd 6497	. . . . . . 7 ⊢ (𝜑 → dom 𝑀 = {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
10	3, 9	eleqtrd 2892	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
11	2, 10	sseldi 3913	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ Word 𝐷)
12		pfxcl 14030	. . . . 5 ⊢ (𝑊 ∈ Word 𝐷 → (𝑊 prefix 𝐸) ∈ Word 𝐷)
13	11, 12	syl 17	. . . 4 ⊢ (𝜑 → (𝑊 prefix 𝐸) ∈ Word 𝐷)
14		cycpmco2.i	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))
15	14	eldifad 3893	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ 𝐷)
16	15	s1cld 13948	. . . 4 ⊢ (𝜑 → ⟨“𝐼”⟩ ∈ Word 𝐷)
17		ccatcl 13917	. . . 4 ⊢ (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ ⟨“𝐼”⟩ ∈ Word 𝐷) → ((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∈ Word 𝐷)
18	13, 16, 17	syl2anc 587	. . 3 ⊢ (𝜑 → ((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∈ Word 𝐷)
19		swrdcl 13998	. . . 4 ⊢ (𝑊 ∈ Word 𝐷 → (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∈ Word 𝐷)
20	11, 19	syl 17	. . 3 ⊢ (𝜑 → (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∈ Word 𝐷)
21		id 22	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
22		dmeq 5736	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → dom 𝑤 = dom 𝑊)
23		eqidd 2799	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → 𝐷 = 𝐷)
24	21, 22, 23	f1eq123d 6583	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑊:dom 𝑊–1-1→𝐷))
25	24	elrab 3628	. . . . . . 7 ⊢ (𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷))
26	10, 25	sylib 221	. . . . . 6 ⊢ (𝜑 → (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷))
27	26	simprd 499	. . . . 5 ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)
28		cycpmco2.e	. . . . . 6 ⊢ 𝐸 = ((^◡𝑊‘𝐽) + 1)
29		f1cnv 6613	. . . . . . . . . 10 ⊢ (𝑊:dom 𝑊–1-1→𝐷 → ^◡𝑊:ran 𝑊–1-1-onto→dom 𝑊)
30		f1of 6590	. . . . . . . . . 10 ⊢ (^◡𝑊:ran 𝑊–1-1-onto→dom 𝑊 → ^◡𝑊:ran 𝑊⟶dom 𝑊)
31	27, 29, 30	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ^◡𝑊:ran 𝑊⟶dom 𝑊)
32		cycpmco2.j	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)
33	31, 32	ffvelrnd 6829	. . . . . . . 8 ⊢ (𝜑 → (^◡𝑊‘𝐽) ∈ dom 𝑊)
34		wrddm 13864	. . . . . . . . 9 ⊢ (𝑊 ∈ Word 𝐷 → dom 𝑊 = (0..^(♯‘𝑊)))
35	11, 34	syl 17	. . . . . . . 8 ⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊)))
36	33, 35	eleqtrd 2892	. . . . . . 7 ⊢ (𝜑 → (^◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊)))
37		fzofzp1 13129	. . . . . . 7 ⊢ ((^◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊)) → ((^◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊)))
38	36, 37	syl 17	. . . . . 6 ⊢ (𝜑 → ((^◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊)))
39	28, 38	eqeltrid 2894	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ (0...(♯‘𝑊)))
40	11, 27, 39	pfxf1 30644	. . . 4 ⊢ (𝜑 → (𝑊 prefix 𝐸):dom (𝑊 prefix 𝐸)–1-1→𝐷)
41	15	s1f1 30645	. . . 4 ⊢ (𝜑 → ⟨“𝐼”⟩:dom ⟨“𝐼”⟩–1-1→𝐷)
42		s1rn 13944	. . . . . . 7 ⊢ (𝐼 ∈ 𝐷 → ran ⟨“𝐼”⟩ = {𝐼})
43	15, 42	syl 17	. . . . . 6 ⊢ (𝜑 → ran ⟨“𝐼”⟩ = {𝐼})
44	43	ineq2d 4139	. . . . 5 ⊢ (𝜑 → (ran (𝑊 prefix 𝐸) ∩ ran ⟨“𝐼”⟩) = (ran (𝑊 prefix 𝐸) ∩ {𝐼}))
45		pfxrn2 30642	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐸) ⊆ ran 𝑊)
46	11, 39, 45	syl2anc 587	. . . . . . . 8 ⊢ (𝜑 → ran (𝑊 prefix 𝐸) ⊆ ran 𝑊)
47	46	ssrind 4162	. . . . . . 7 ⊢ (𝜑 → (ran (𝑊 prefix 𝐸) ∩ {𝐼}) ⊆ (ran 𝑊 ∩ {𝐼}))
48	14	eldifbd 3894	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝐼 ∈ ran 𝑊)
49		disjsn 4607	. . . . . . . 8 ⊢ ((ran 𝑊 ∩ {𝐼}) = ∅ ↔ ¬ 𝐼 ∈ ran 𝑊)
50	48, 49	sylibr 237	. . . . . . 7 ⊢ (𝜑 → (ran 𝑊 ∩ {𝐼}) = ∅)
51	47, 50	sseqtrd 3955	. . . . . 6 ⊢ (𝜑 → (ran (𝑊 prefix 𝐸) ∩ {𝐼}) ⊆ ∅)
52		ss0 4306	. . . . . 6 ⊢ ((ran (𝑊 prefix 𝐸) ∩ {𝐼}) ⊆ ∅ → (ran (𝑊 prefix 𝐸) ∩ {𝐼}) = ∅)
53	51, 52	syl 17	. . . . 5 ⊢ (𝜑 → (ran (𝑊 prefix 𝐸) ∩ {𝐼}) = ∅)
54	44, 53	eqtrd 2833	. . . 4 ⊢ (𝜑 → (ran (𝑊 prefix 𝐸) ∩ ran ⟨“𝐼”⟩) = ∅)
55	1, 13, 16, 40, 41, 54	ccatf1 30651	. . 3 ⊢ (𝜑 → ((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩):dom ((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩)–1-1→𝐷)
56		lencl 13876	. . . . 5 ⊢ (𝑊 ∈ Word 𝐷 → (♯‘𝑊) ∈ ℕ₀)
57		nn0fz0 13000	. . . . . 6 ⊢ ((♯‘𝑊) ∈ ℕ₀ ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊)))
58	57	biimpi 219	. . . . 5 ⊢ ((♯‘𝑊) ∈ ℕ₀ → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
59	11, 56, 58	3syl 18	. . . 4 ⊢ (𝜑 → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
60	11, 39, 59, 27	swrdf1 30656	. . 3 ⊢ (𝜑 → (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩):dom (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)–1-1→𝐷)
61		ccatrn 13934	. . . . . . 7 ⊢ (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ ⟨“𝐼”⟩ ∈ Word 𝐷) → ran ((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) = (ran (𝑊 prefix 𝐸) ∪ ran ⟨“𝐼”⟩))
62	13, 16, 61	syl2anc 587	. . . . . 6 ⊢ (𝜑 → ran ((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) = (ran (𝑊 prefix 𝐸) ∪ ran ⟨“𝐼”⟩))
63	62	ineq1d 4138	. . . . 5 ⊢ (𝜑 → (ran ((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∩ ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) = ((ran (𝑊 prefix 𝐸) ∪ ran ⟨“𝐼”⟩) ∩ ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))
64		indir 4202	. . . . 5 ⊢ ((ran (𝑊 prefix 𝐸) ∪ ran ⟨“𝐼”⟩) ∩ ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) = ((ran (𝑊 prefix 𝐸) ∩ ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) ∪ (ran ⟨“𝐼”⟩ ∩ ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))
65	63, 64	eqtrdi 2849	. . . 4 ⊢ (𝜑 → (ran ((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∩ ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) = ((ran (𝑊 prefix 𝐸) ∩ ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) ∪ (ran ⟨“𝐼”⟩ ∩ ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))))
66		fz0ssnn0 12997	. . . . . . . . . 10 ⊢ (0...(♯‘𝑊)) ⊆ ℕ₀
67	66, 39	sseldi 3913	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ ℕ₀)
68		pfxval 14026	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ℕ₀) → (𝑊 prefix 𝐸) = (𝑊 substr ⟨0, 𝐸⟩))
69	11, 67, 68	syl2anc 587	. . . . . . . 8 ⊢ (𝜑 → (𝑊 prefix 𝐸) = (𝑊 substr ⟨0, 𝐸⟩))
70	69	rneqd 5772	. . . . . . 7 ⊢ (𝜑 → ran (𝑊 prefix 𝐸) = ran (𝑊 substr ⟨0, 𝐸⟩))
71	70	ineq1d 4138	. . . . . 6 ⊢ (𝜑 → (ran (𝑊 prefix 𝐸) ∩ ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) = (ran (𝑊 substr ⟨0, 𝐸⟩) ∩ ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))
72		0elfz 12999	. . . . . . . 8 ⊢ (𝐸 ∈ ℕ₀ → 0 ∈ (0...𝐸))
73	67, 72	syl 17	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0...𝐸))
74		elfzuz3 12899	. . . . . . . 8 ⊢ (𝐸 ∈ (0...(♯‘𝑊)) → (♯‘𝑊) ∈ (ℤ_≥‘𝐸))
75		eluzfz1 12909	. . . . . . . 8 ⊢ ((♯‘𝑊) ∈ (ℤ_≥‘𝐸) → 𝐸 ∈ (𝐸...(♯‘𝑊)))
76	39, 74, 75	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ (𝐸...(♯‘𝑊)))
77		eluzfz2 12910	. . . . . . . 8 ⊢ ((♯‘𝑊) ∈ (ℤ_≥‘𝐸) → (♯‘𝑊) ∈ (𝐸...(♯‘𝑊)))
78	39, 74, 77	3syl 18	. . . . . . 7 ⊢ (𝜑 → (♯‘𝑊) ∈ (𝐸...(♯‘𝑊)))
79	11, 73, 39, 27, 76, 78	swrdrndisj 30657	. . . . . 6 ⊢ (𝜑 → (ran (𝑊 substr ⟨0, 𝐸⟩) ∩ ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) = ∅)
80	71, 79	eqtrd 2833	. . . . 5 ⊢ (𝜑 → (ran (𝑊 prefix 𝐸) ∩ ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) = ∅)
81		incom 4128	. . . . . 6 ⊢ (ran ⟨“𝐼”⟩ ∩ ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) = (ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∩ ran ⟨“𝐼”⟩)
82	43	ineq2d 4139	. . . . . . 7 ⊢ (𝜑 → (ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∩ ran ⟨“𝐼”⟩) = (ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∩ {𝐼}))
83		swrdrn2 30654	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈ (0...(♯‘𝑊))) → ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ⊆ ran 𝑊)
84	11, 39, 59, 83	syl3anc 1368	. . . . . . . . . 10 ⊢ (𝜑 → ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ⊆ ran 𝑊)
85	84	ssrind 4162	. . . . . . . . 9 ⊢ (𝜑 → (ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∩ {𝐼}) ⊆ (ran 𝑊 ∩ {𝐼}))
86	85, 50	sseqtrd 3955	. . . . . . . 8 ⊢ (𝜑 → (ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∩ {𝐼}) ⊆ ∅)
87		ss0 4306	. . . . . . . 8 ⊢ ((ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∩ {𝐼}) ⊆ ∅ → (ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∩ {𝐼}) = ∅)
88	86, 87	syl 17	. . . . . . 7 ⊢ (𝜑 → (ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∩ {𝐼}) = ∅)
89	82, 88	eqtrd 2833	. . . . . 6 ⊢ (𝜑 → (ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩) ∩ ran ⟨“𝐼”⟩) = ∅)
90	81, 89	syl5eq 2845	. . . . 5 ⊢ (𝜑 → (ran ⟨“𝐼”⟩ ∩ ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) = ∅)
91	80, 90	uneq12d 4091	. . . 4 ⊢ (𝜑 → ((ran (𝑊 prefix 𝐸) ∩ ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) ∪ (ran ⟨“𝐼”⟩ ∩ ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))) = (∅ ∪ ∅))
92		unidm 4079	. . . . 5 ⊢ (∅ ∪ ∅) = ∅
93	92	a1i 11	. . . 4 ⊢ (𝜑 → (∅ ∪ ∅) = ∅)
94	65, 91, 93	3eqtrd 2837	. . 3 ⊢ (𝜑 → (ran ((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ∩ ran (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)) = ∅)
95	1, 18, 20, 55, 60, 94	ccatf1 30651	. 2 ⊢ (𝜑 → (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)):dom (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))–1-1→𝐷)
96		cycpmco2.1	. . . 4 ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)
97		ovexd 7170	. . . . . 6 ⊢ (𝜑 → ((^◡𝑊‘𝐽) + 1) ∈ V)
98	28, 97	eqeltrid 2894	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ V)
99		splval 14104	. . . . 5 ⊢ ((𝑊 ∈ dom 𝑀 ∧ (𝐸 ∈ V ∧ 𝐸 ∈ V ∧ ⟨“𝐼”⟩ ∈ Word 𝐷)) → (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))
100	3, 98, 98, 16, 99	syl13anc 1369	. . . 4 ⊢ (𝜑 → (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))
101	96, 100	syl5eq 2845	. . 3 ⊢ (𝜑 → 𝑈 = (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))
102	101	dmeqd 5738	. . 3 ⊢ (𝜑 → dom 𝑈 = dom (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)))
103		eqidd 2799	. . 3 ⊢ (𝜑 → 𝐷 = 𝐷)
104	101, 102, 103	f1eq123d 6583	. 2 ⊢ (𝜑 → (𝑈:dom 𝑈–1-1→𝐷 ↔ (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩)):dom (((𝑊 prefix 𝐸) ++ ⟨“𝐼”⟩) ++ (𝑊 substr ⟨𝐸, (♯‘𝑊)⟩))–1-1→𝐷))
105	95, 104	mpbird 260	1 ⊢ (𝜑 → 𝑈:dom 𝑈–1-1→𝐷)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 = wceq 1538 ∈ wcel 2111 {crab 3110 Vcvv 3441 ∖ cdif 3878 ∪ cun 3879 ∩ cin 3880 ⊆ wss 3881 ∅c0 4243 {csn 4525 ⟨cop 4531 ⟨cotp 4533 ^◡ccnv 5518 dom cdm 5519 ran crn 5520 ⟶wf 6320 –1-1→wf1 6321 –1-1-onto→wf1o 6323 ‘cfv 6324 (class class class)co 7135 0cc0 10526 1c1 10527 + caddc 10529 ℕ₀cn0 11885 ℤ_≥cuz 12231 ...cfz 12885 ..^cfzo 13028 ♯chash 13686 Word cword 13857 ++ cconcat 13913 ⟨“cs1 13940 substr csubstr 13993 prefix cpfx 14023 splice csplice 14102 Basecbs 16475 SymGrpcsymg 18487 toCycctocyc 30798

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603 ax-pre-sup 10604

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-ot 4534 df-uni 4801 df-int 4839 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-om 7561 df-1st 7671 df-2nd 7672 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-1o 8085 df-oadd 8089 df-er 8272 df-map 8391 df-en 8493 df-dom 8494 df-sdom 8495 df-fin 8496 df-sup 8890 df-inf 8891 df-card 9352 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-div 11287 df-nn 11626 df-2 11688 df-3 11689 df-4 11690 df-5 11691 df-6 11692 df-7 11693 df-8 11694 df-9 11695 df-n0 11886 df-z 11970 df-uz 12232 df-rp 12378 df-fz 12886 df-fzo 13029 df-fl 13157 df-mod 13233 df-hash 13687 df-word 13858 df-concat 13914 df-s1 13941 df-substr 13994 df-pfx 14024 df-splice 14103 df-csh 14142 df-struct 16477 df-ndx 16478 df-slot 16479 df-base 16481 df-sets 16482 df-ress 16483 df-plusg 16570 df-tset 16576 df-efmnd 18026 df-symg 18488 df-tocyc 30799

This theorem is referenced by: cycpmco2lem4 30821 cycpmco2lem5 30822 cycpmco2lem6 30823 cycpmco2lem7 30824 cycpmco2 30825

W3C validator