cshf1 - Metamath Proof Explorer

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

Theorem cshf1 14965

Description: Cyclically shifting a word which contains a symbol at most once results in a word which contains a symbol at most once. (Contributed by AV, 14-Mar-2021.)

**Assertion**
Ref	Expression
cshf1	⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → 𝐺:(0..^(♯‘𝐹))–1-1→𝐴)

Proof of Theorem cshf1 Dummy variables 𝑖 𝑗 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1f 6778	. . . . 5 ⊢ (𝐹:(0..^(♯‘𝐹))–1-1→𝐴 → 𝐹:(0..^(♯‘𝐹))⟶𝐴)
2		iswrdi 14665	. . . . 5 ⊢ (𝐹:(0..^(♯‘𝐹))⟶𝐴 → 𝐹 ∈ Word 𝐴)
3	1, 2	syl 18	. . . 4 ⊢ (𝐹:(0..^(♯‘𝐹))–1-1→𝐴 → 𝐹 ∈ Word 𝐴)
4		cshwf 14955	. . . . . . . . 9 ⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐹 cyclShift 𝑆):(0..^(♯‘𝐹))⟶𝐴)
5	4	3adant1 1148	. . . . . . . 8 ⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐹 cyclShift 𝑆):(0..^(♯‘𝐹))⟶𝐴)
6	5	adantr 486	. . . . . . 7 ⊢ (((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐹 cyclShift 𝑆):(0..^(♯‘𝐹))⟶𝐴)
7		feq1 6687	. . . . . . . 8 ⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺:(0..^(♯‘𝐹))⟶𝐴 ↔ (𝐹 cyclShift 𝑆):(0..^(♯‘𝐹))⟶𝐴))
8	7	adantl 487	. . . . . . 7 ⊢ (((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐺:(0..^(♯‘𝐹))⟶𝐴 ↔ (𝐹 cyclShift 𝑆):(0..^(♯‘𝐹))⟶𝐴))
9	6, 8	mpbird 260	. . . . . 6 ⊢ (((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → 𝐺:(0..^(♯‘𝐹))⟶𝐴)
10		dff13 7258	. . . . . . . 8 ⊢ (𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ↔ (𝐹:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
11		fveq1 6884	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺‘𝑖) = ((𝐹 cyclShift 𝑆)‘𝑖))
12	11	3ad2ant1 1151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐺‘𝑖) = ((𝐹 cyclShift 𝑆)‘𝑖))
13	12	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (𝐺‘𝑖) = ((𝐹 cyclShift 𝑆)‘𝑖))
14		cshwidxmod 14958	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝑖 ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))))
15	14	3expia 1139	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑖 ∈ (0..^(♯‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹)))))
16	15	3adant1 1148	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑖 ∈ (0..^(♯‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹)))))
17	16	com12 33	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (0..^(♯‘𝐹)) → ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹)))))
18	17	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹))) → ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹)))))
19	18	impcom 413	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))))
20	13, 19	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (𝐺‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))))
21		fveq1 6884	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺‘𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗))
22	21	3ad2ant1 1151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐺‘𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗))
23	22	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (𝐺‘𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗))
24		cshwidxmod 14958	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝑗 ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))))
25	24	3expia 1139	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑗 ∈ (0..^(♯‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹)))))
26	25	3adant1 1148	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑗 ∈ (0..^(♯‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹)))))
27	26	adantld 496	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹)))))
28	27	imp 412	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))))
29	23, 28	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (𝐺‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))))
30	20, 29	eqeq12d 2776	. . . . . . . . . . . . . 14 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐺‘𝑖) = (𝐺‘𝑗) ↔ (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹)))))
31	30	adantlr 728	. . . . . . . . . . . . 13 ⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐺‘𝑖) = (𝐺‘𝑗) ↔ (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹)))))
32		elfzo0 13838	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^(♯‘𝐹)) ↔ (𝑖 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑖 < (♯‘𝐹)))
33		nn0z 12720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 ∈ ℕ₀ → 𝑖 ∈ ℤ)
34	33	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑖 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ) → 𝑖 ∈ ℤ)
35	34	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ)) → 𝑖 ∈ ℤ)
36		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ)) → 𝑆 ∈ ℤ)
37	35, 36	zaddcld 12810	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ)) → (𝑖 + 𝑆) ∈ ℤ)
38		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑖 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ) → (♯‘𝐹) ∈ ℕ)
39	38	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ)) → (♯‘𝐹) ∈ ℕ)
40	37, 39	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ)) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ))
41	40	ex 418	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑆 ∈ ℤ → ((𝑖 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ)))
42	41	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ)))
43	42	com12 33	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑖 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ) → ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ)))
44	43	3adant3 1150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑖 < (♯‘𝐹)) → ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ)))
45	32, 44	sylbi 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^(♯‘𝐹)) → ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ)))
46	45	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹))) → ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ)))
47	46	impcom 413	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ))
48		zmodfzo 14037	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ) → ((𝑖 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹)))
49	47, 48	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹)))
50		elfzo0 13838	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ (0..^(♯‘𝐹)) ↔ (𝑗 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑗 < (♯‘𝐹)))
51		nn0z 12720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 ∈ ℕ₀ → 𝑗 ∈ ℤ)
52	51	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑗 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ) → 𝑗 ∈ ℤ)
53	52	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ)) → 𝑗 ∈ ℤ)
54		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ)) → 𝑆 ∈ ℤ)
55	53, 54	zaddcld 12810	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ)) → (𝑗 + 𝑆) ∈ ℤ)
56		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ) → (♯‘𝐹) ∈ ℕ)
57	56	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ)) → (♯‘𝐹) ∈ ℕ)
58	55, 57	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ)) → ((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ))
59	58	expcom 419	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑗 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ) → (𝑆 ∈ ℤ → ((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ)))
60	59	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑗 ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑗 < (♯‘𝐹)) → (𝑆 ∈ ℤ → ((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ)))
61	50, 60	sylbi 220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0..^(♯‘𝐹)) → (𝑆 ∈ ℤ → ((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ)))
62	61	com12 33	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ ℤ → (𝑗 ∈ (0..^(♯‘𝐹)) → ((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ)))
63	62	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑗 ∈ (0..^(♯‘𝐹)) → ((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ)))
64	63	adantld 496	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹))) → ((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ)))
65	64	imp 412	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ))
66		zmodfzo 14037	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑗 + 𝑆) ∈ ℤ ∧ (♯‘𝐹) ∈ ℕ) → ((𝑗 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹)))
67	65, 66	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝑗 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹)))
68		fveqeq2 6894	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = ((𝑖 + 𝑆) mod (♯‘𝐹)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘𝑦)))
69		eqeq1 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = ((𝑖 + 𝑆) mod (♯‘𝐹)) → (𝑥 = 𝑦 ↔ ((𝑖 + 𝑆) mod (♯‘𝐹)) = 𝑦))
70	68, 69	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = ((𝑖 + 𝑆) mod (♯‘𝐹)) → (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘𝑦) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = 𝑦)))
71		fveq2 6885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((𝑗 + 𝑆) mod (♯‘𝐹)) → (𝐹‘𝑦) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))))
72	71	eqeq2d 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑗 + 𝑆) mod (♯‘𝐹)) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘𝑦) ↔ (𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹)))))
73		eqeq2 2772	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑗 + 𝑆) mod (♯‘𝐹)) → (((𝑖 + 𝑆) mod (♯‘𝐹)) = 𝑦 ↔ ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹))))
74	72, 73	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑗 + 𝑆) mod (♯‘𝐹)) → (((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘𝑦) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = 𝑦) ↔ ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))))
75	70, 74	rspc2v 3586	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑖 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹)) ∧ ((𝑗 + 𝑆) mod (♯‘𝐹)) ∈ (0..^(♯‘𝐹))) → (∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))))
76	49, 67, 75	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))))
77		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) ∧ ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹))))
78		addmodlteq 14092	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)) ∧ 𝑆 ∈ ℤ) → (((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)) ↔ 𝑖 = 𝑗))
79	78	3expa 1136	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹))) ∧ 𝑆 ∈ ℤ) → (((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)) ↔ 𝑖 = 𝑗))
80	79	ancoms 464	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)) ↔ 𝑖 = 𝑗))
81	80	bicomd 226	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹))))
82	81	3ad2antl3 1206	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹))))
83	82	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) ∧ ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) → (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹))))
84	77, 83	sylibrd 262	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) ∧ ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹)))) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → 𝑖 = 𝑗))
85	84	ex 418	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝑖 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod (♯‘𝐹))) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → 𝑖 = 𝑗)))
86	76, 85	syld 48	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → (∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → 𝑖 = 𝑗)))
87	86	impancom 457	. . . . . . . . . . . . . 14 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) → ((𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹))) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → 𝑖 = 𝑗)))
88	87	imp 412	. . . . . . . . . . . . 13 ⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐹‘((𝑖 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) → 𝑖 = 𝑗))
89	31, 88	sylbid 243	. . . . . . . . . . . 12 ⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ∧ (𝑖 ∈ (0..^(♯‘𝐹)) ∧ 𝑗 ∈ (0..^(♯‘𝐹)))) → ((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))
90	89	ralrimivva 3205	. . . . . . . . . . 11 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))
91	90	3exp1 1371	. . . . . . . . . 10 ⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))))
92	91	com14 97	. . . . . . . . 9 ⊢ (∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))))
93	92	adantl 487	. . . . . . . 8 ⊢ ((𝐹:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))))
94	10, 93	sylbi 220	. . . . . . 7 ⊢ (𝐹:(0..^(♯‘𝐹))–1-1→𝐴 → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))))
95	94	3imp1 1366	. . . . . 6 ⊢ (((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))
96	9, 95	jca 521	. . . . 5 ⊢ (((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐺:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))
97	96	3exp1 1371	. . . 4 ⊢ (𝐹:(0..^(♯‘𝐹))–1-1→𝐴 → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))))))
98	3, 97	mpd 16	. . 3 ⊢ (𝐹:(0..^(♯‘𝐹))–1-1→𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))))
99	98	3imp 1128	. 2 ⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐺:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))
100		dff13 7258	. 2 ⊢ (𝐺:(0..^(♯‘𝐹))–1-1→𝐴 ↔ (𝐺:(0..^(♯‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))∀𝑗 ∈ (0..^(♯‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))
101	99, 100	sylibr 237	1 ⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → 𝐺:(0..^(♯‘𝐹))–1-1→𝐴)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∀wral 3076 class class class wbr 5102 ⟶wf 6534 –1-1→wf1 6535 ‘cfv 6538 (class class class)co 7420 0cc0 11203 + caddc 11206 < clt 11346 ℕcn 12338 ℕ₀cn0 12609 ℤcz 12696 ..^cfzo 13791 mod cmo 14012 ♯chash 14477 Word cword 14661 cyclShift ccsh 14943

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11259 ax-resscn 11260 ax-1cn 11261 ax-icn 11262 ax-addcl 11263 ax-addrcl 11264 ax-mulcl 11265 ax-mulrcl 11266 ax-mulcom 11267 ax-addass 11268 ax-mulass 11269 ax-distr 11270 ax-i2m1 11271 ax-1ne0 11272 ax-1rid 11273 ax-rnegex 11274 ax-rrecex 11275 ax-cnre 11276 ax-pre-lttri 11277 ax-pre-lttrn 11278 ax-pre-ltadd 11279 ax-pre-mulgt0 11280 ax-pre-sup 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-1o 8479 df-er 8720 df-en 8977 df-dom 8978 df-sdom 8979 df-fin 8980 df-sup 9437 df-inf 9438 df-card 10023 df-pnf 11348 df-mnf 11349 df-xr 11350 df-ltxr 11351 df-le 11352 df-sub 11546 df-neg 11547 df-div 11977 df-nn 12339 df-2 12408 df-n0 12610 df-z 12697 df-uz 12969 df-rp 13124 df-fz 13643 df-fzo 13792 df-fl 13935 df-mod 14013 df-hash 14478 df-word 14662 df-concat 14719 df-substr 14793 df-pfx 14825 df-csh 14944

This theorem is used by: cshinj 14966 cshf1o 33569

W3C validator