Step |
Hyp |
Ref |
Expression |
1 |
|
efgval.w |
⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) ) |
2 |
|
efgval.r |
⊢ ∼ = ( ~FG ‘ 𝐼 ) |
3 |
|
efgval2.m |
⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 ) |
4 |
|
efgval2.t |
⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice 〈 𝑛 , 𝑛 , 〈“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”〉 〉 ) ) ) |
5 |
|
efgred.d |
⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) |
6 |
|
efgred.s |
⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) ) |
7 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 0 ) ) |
8 |
7
|
eleq1d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 0 ) ∈ 𝐷 ↔ ( 𝐹 ‘ 0 ) ∈ 𝐷 ) ) |
9 |
|
fveq2 |
⊢ ( 𝑓 = 𝐹 → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ 𝐹 ) ) |
10 |
9
|
oveq2d |
⊢ ( 𝑓 = 𝐹 → ( 1 ..^ ( ♯ ‘ 𝑓 ) ) = ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) |
11 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑖 ) ) |
12 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑖 − 1 ) ) = ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) |
13 |
12
|
fveq2d |
⊢ ( 𝑓 = 𝐹 → ( 𝑇 ‘ ( 𝑓 ‘ ( 𝑖 − 1 ) ) ) = ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) ) |
14 |
13
|
rneqd |
⊢ ( 𝑓 = 𝐹 → ran ( 𝑇 ‘ ( 𝑓 ‘ ( 𝑖 − 1 ) ) ) = ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) ) |
15 |
11 14
|
eleq12d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝑓 ‘ ( 𝑖 − 1 ) ) ) ↔ ( 𝐹 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) ) ) |
16 |
10 15
|
raleqbidv |
⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝑓 ‘ ( 𝑖 − 1 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) ) ) |
17 |
8 16
|
anbi12d |
⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝑓 ‘ ( 𝑖 − 1 ) ) ) ) ↔ ( ( 𝐹 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) ) ) ) |
18 |
1 2 3 4 5 6
|
efgsf |
⊢ 𝑆 : { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ⟶ 𝑊 |
19 |
18
|
fdmi |
⊢ dom 𝑆 = { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } |
20 |
|
fveq1 |
⊢ ( 𝑡 = 𝑓 → ( 𝑡 ‘ 0 ) = ( 𝑓 ‘ 0 ) ) |
21 |
20
|
eleq1d |
⊢ ( 𝑡 = 𝑓 → ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ↔ ( 𝑓 ‘ 0 ) ∈ 𝐷 ) ) |
22 |
|
fveq2 |
⊢ ( 𝑘 = 𝑖 → ( 𝑡 ‘ 𝑘 ) = ( 𝑡 ‘ 𝑖 ) ) |
23 |
|
fvoveq1 |
⊢ ( 𝑘 = 𝑖 → ( 𝑡 ‘ ( 𝑘 − 1 ) ) = ( 𝑡 ‘ ( 𝑖 − 1 ) ) ) |
24 |
23
|
fveq2d |
⊢ ( 𝑘 = 𝑖 → ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) = ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑖 − 1 ) ) ) ) |
25 |
24
|
rneqd |
⊢ ( 𝑘 = 𝑖 → ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) = ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑖 − 1 ) ) ) ) |
26 |
22 25
|
eleq12d |
⊢ ( 𝑘 = 𝑖 → ( ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ↔ ( 𝑡 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑖 − 1 ) ) ) ) ) |
27 |
26
|
cbvralvw |
⊢ ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑖 − 1 ) ) ) ) |
28 |
|
fveq2 |
⊢ ( 𝑡 = 𝑓 → ( ♯ ‘ 𝑡 ) = ( ♯ ‘ 𝑓 ) ) |
29 |
28
|
oveq2d |
⊢ ( 𝑡 = 𝑓 → ( 1 ..^ ( ♯ ‘ 𝑡 ) ) = ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) |
30 |
|
fveq1 |
⊢ ( 𝑡 = 𝑓 → ( 𝑡 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ) |
31 |
|
fveq1 |
⊢ ( 𝑡 = 𝑓 → ( 𝑡 ‘ ( 𝑖 − 1 ) ) = ( 𝑓 ‘ ( 𝑖 − 1 ) ) ) |
32 |
31
|
fveq2d |
⊢ ( 𝑡 = 𝑓 → ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑖 − 1 ) ) ) = ( 𝑇 ‘ ( 𝑓 ‘ ( 𝑖 − 1 ) ) ) ) |
33 |
32
|
rneqd |
⊢ ( 𝑡 = 𝑓 → ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑖 − 1 ) ) ) = ran ( 𝑇 ‘ ( 𝑓 ‘ ( 𝑖 − 1 ) ) ) ) |
34 |
30 33
|
eleq12d |
⊢ ( 𝑡 = 𝑓 → ( ( 𝑡 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑖 − 1 ) ) ) ↔ ( 𝑓 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝑓 ‘ ( 𝑖 − 1 ) ) ) ) ) |
35 |
29 34
|
raleqbidv |
⊢ ( 𝑡 = 𝑓 → ( ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑖 − 1 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝑓 ‘ ( 𝑖 − 1 ) ) ) ) ) |
36 |
27 35
|
syl5bb |
⊢ ( 𝑡 = 𝑓 → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝑓 ‘ ( 𝑖 − 1 ) ) ) ) ) |
37 |
21 36
|
anbi12d |
⊢ ( 𝑡 = 𝑓 → ( ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) ↔ ( ( 𝑓 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝑓 ‘ ( 𝑖 − 1 ) ) ) ) ) ) |
38 |
37
|
cbvrabv |
⊢ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } = { 𝑓 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑓 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝑓 ‘ ( 𝑖 − 1 ) ) ) ) } |
39 |
19 38
|
eqtri |
⊢ dom 𝑆 = { 𝑓 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑓 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝑓 ‘ ( 𝑖 − 1 ) ) ) ) } |
40 |
17 39
|
elrab2 |
⊢ ( 𝐹 ∈ dom 𝑆 ↔ ( 𝐹 ∈ ( Word 𝑊 ∖ { ∅ } ) ∧ ( ( 𝐹 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) ) ) ) |
41 |
|
3anass |
⊢ ( ( 𝐹 ∈ ( Word 𝑊 ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) ) ↔ ( 𝐹 ∈ ( Word 𝑊 ∖ { ∅ } ) ∧ ( ( 𝐹 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) ) ) ) |
42 |
40 41
|
bitr4i |
⊢ ( 𝐹 ∈ dom 𝑆 ↔ ( 𝐹 ∈ ( Word 𝑊 ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) ) ) |