Step |
Hyp |
Ref |
Expression |
1 |
|
tocycval.1 |
⊢ 𝐶 = ( toCyc ‘ 𝐷 ) |
2 |
|
df-tocyc |
⊢ toCyc = ( 𝑑 ∈ V ↦ ( 𝑤 ∈ { 𝑢 ∈ Word 𝑑 ∣ 𝑢 : dom 𝑢 –1-1→ 𝑑 } ↦ ( ( I ↾ ( 𝑑 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) ) |
3 |
|
wrdeq |
⊢ ( 𝑑 = 𝐷 → Word 𝑑 = Word 𝐷 ) |
4 |
|
f1eq3 |
⊢ ( 𝑑 = 𝐷 → ( 𝑢 : dom 𝑢 –1-1→ 𝑑 ↔ 𝑢 : dom 𝑢 –1-1→ 𝐷 ) ) |
5 |
3 4
|
rabeqbidv |
⊢ ( 𝑑 = 𝐷 → { 𝑢 ∈ Word 𝑑 ∣ 𝑢 : dom 𝑢 –1-1→ 𝑑 } = { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } ) |
6 |
|
difeq1 |
⊢ ( 𝑑 = 𝐷 → ( 𝑑 ∖ ran 𝑤 ) = ( 𝐷 ∖ ran 𝑤 ) ) |
7 |
6
|
reseq2d |
⊢ ( 𝑑 = 𝐷 → ( I ↾ ( 𝑑 ∖ ran 𝑤 ) ) = ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ) |
8 |
7
|
uneq1d |
⊢ ( 𝑑 = 𝐷 → ( ( I ↾ ( 𝑑 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) |
9 |
5 8
|
mpteq12dv |
⊢ ( 𝑑 = 𝐷 → ( 𝑤 ∈ { 𝑢 ∈ Word 𝑑 ∣ 𝑢 : dom 𝑢 –1-1→ 𝑑 } ↦ ( ( I ↾ ( 𝑑 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) = ( 𝑤 ∈ { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } ↦ ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) ) |
10 |
|
elex |
⊢ ( 𝐷 ∈ 𝑉 → 𝐷 ∈ V ) |
11 |
|
eqid |
⊢ { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } = { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } |
12 |
|
wrdexg |
⊢ ( 𝐷 ∈ 𝑉 → Word 𝐷 ∈ V ) |
13 |
11 12
|
rabexd |
⊢ ( 𝐷 ∈ 𝑉 → { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } ∈ V ) |
14 |
13
|
mptexd |
⊢ ( 𝐷 ∈ 𝑉 → ( 𝑤 ∈ { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } ↦ ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) ∈ V ) |
15 |
2 9 10 14
|
fvmptd3 |
⊢ ( 𝐷 ∈ 𝑉 → ( toCyc ‘ 𝐷 ) = ( 𝑤 ∈ { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } ↦ ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) ) |
16 |
1 15
|
syl5eq |
⊢ ( 𝐷 ∈ 𝑉 → 𝐶 = ( 𝑤 ∈ { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } ↦ ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) ) |