Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . . . . . . . 10
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) |
2 | | fviss 6734 |
. . . . . . . . . 10
⊢ ( I
‘Word (𝐼 ×
2o)) ⊆ Word (𝐼 × 2o) |
3 | 1, 2 | eqsstri 3998 |
. . . . . . . . 9
⊢ 𝑊 ⊆ Word (𝐼 × 2o) |
4 | | simpl 483 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2o))) → 𝑋 ∈ 𝑊) |
5 | 3, 4 | sseldi 3962 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2o))) → 𝑋 ∈ Word (𝐼 × 2o)) |
6 | | simprr 769 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2o))) → 𝑏 ∈ (𝐼 × 2o)) |
7 | | efgval2.m |
. . . . . . . . . . . 12
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) |
8 | 7 | efgmf 18768 |
. . . . . . . . . . 11
⊢ 𝑀:(𝐼 × 2o)⟶(𝐼 ×
2o) |
9 | 8 | ffvelrni 6842 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (𝐼 × 2o) → (𝑀‘𝑏) ∈ (𝐼 × 2o)) |
10 | 9 | ad2antll 725 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2o))) → (𝑀‘𝑏) ∈ (𝐼 × 2o)) |
11 | 6, 10 | s2cld 14221 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2o))) →
〈“𝑏(𝑀‘𝑏)”〉 ∈ Word (𝐼 × 2o)) |
12 | | splcl 14102 |
. . . . . . . 8
⊢ ((𝑋 ∈ Word (𝐼 × 2o) ∧
〈“𝑏(𝑀‘𝑏)”〉 ∈ Word (𝐼 × 2o)) → (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) ∈ Word (𝐼 ×
2o)) |
13 | 5, 11, 12 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2o))) → (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) ∈ Word (𝐼 ×
2o)) |
14 | 1 | efgrcl 18770 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o))) |
15 | 14 | simprd 496 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑊 → 𝑊 = Word (𝐼 × 2o)) |
16 | 15 | adantr 481 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2o))) → 𝑊 = Word (𝐼 × 2o)) |
17 | 13, 16 | eleqtrrd 2913 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2o))) → (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) ∈ 𝑊) |
18 | 17 | ralrimivva 3188 |
. . . . 5
⊢ (𝑋 ∈ 𝑊 → ∀𝑎 ∈ (0...(♯‘𝑋))∀𝑏 ∈ (𝐼 × 2o)(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) ∈ 𝑊) |
19 | | eqid 2818 |
. . . . . 6
⊢ (𝑎 ∈
(0...(♯‘𝑋)),
𝑏 ∈ (𝐼 × 2o) ↦ (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) = (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) |
20 | 19 | fmpo 7755 |
. . . . 5
⊢
(∀𝑎 ∈
(0...(♯‘𝑋))∀𝑏 ∈ (𝐼 × 2o)(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) ∈ 𝑊 ↔ (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)):((0...(♯‘𝑋)) × (𝐼 × 2o))⟶𝑊) |
21 | 18, 20 | sylib 219 |
. . . 4
⊢ (𝑋 ∈ 𝑊 → (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)):((0...(♯‘𝑋)) × (𝐼 × 2o))⟶𝑊) |
22 | | ovex 7178 |
. . . . 5
⊢
(0...(♯‘𝑋)) ∈ V |
23 | 14 | simpld 495 |
. . . . . 6
⊢ (𝑋 ∈ 𝑊 → 𝐼 ∈ V) |
24 | | 2on 8100 |
. . . . . 6
⊢
2o ∈ On |
25 | | xpexg 7462 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 2o
∈ On) → (𝐼
× 2o) ∈ V) |
26 | 23, 24, 25 | sylancl 586 |
. . . . 5
⊢ (𝑋 ∈ 𝑊 → (𝐼 × 2o) ∈
V) |
27 | | xpexg 7462 |
. . . . 5
⊢
(((0...(♯‘𝑋)) ∈ V ∧ (𝐼 × 2o) ∈ V) →
((0...(♯‘𝑋))
× (𝐼 ×
2o)) ∈ V) |
28 | 22, 26, 27 | sylancr 587 |
. . . 4
⊢ (𝑋 ∈ 𝑊 → ((0...(♯‘𝑋)) × (𝐼 × 2o)) ∈
V) |
29 | 1 | fvexi 6677 |
. . . . 5
⊢ 𝑊 ∈ V |
30 | 29 | a1i 11 |
. . . 4
⊢ (𝑋 ∈ 𝑊 → 𝑊 ∈ V) |
31 | | fex2 7627 |
. . . 4
⊢ (((𝑎 ∈
(0...(♯‘𝑋)),
𝑏 ∈ (𝐼 × 2o) ↦ (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)):((0...(♯‘𝑋)) × (𝐼 × 2o))⟶𝑊 ∧ ((0...(♯‘𝑋)) × (𝐼 × 2o)) ∈ V ∧ 𝑊 ∈ V) → (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∈ V) |
32 | 21, 28, 30, 31 | syl3anc 1363 |
. . 3
⊢ (𝑋 ∈ 𝑊 → (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∈
V) |
33 | | fveq2 6663 |
. . . . . 6
⊢ (𝑢 = 𝑋 → (♯‘𝑢) = (♯‘𝑋)) |
34 | 33 | oveq2d 7161 |
. . . . 5
⊢ (𝑢 = 𝑋 → (0...(♯‘𝑢)) = (0...(♯‘𝑋))) |
35 | | eqidd 2819 |
. . . . 5
⊢ (𝑢 = 𝑋 → (𝐼 × 2o) = (𝐼 × 2o)) |
36 | | oveq1 7152 |
. . . . 5
⊢ (𝑢 = 𝑋 → (𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) = (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) |
37 | 34, 35, 36 | mpoeq123dv 7218 |
. . . 4
⊢ (𝑢 = 𝑋 → (𝑎 ∈ (0...(♯‘𝑢)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) = (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
38 | | efgval2.t |
. . . . 5
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
39 | | oteq1 4804 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑎 → 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉 = 〈𝑎, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉) |
40 | | oteq2 4805 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑎 → 〈𝑎, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉 = 〈𝑎, 𝑎, 〈“𝑤(𝑀‘𝑤)”〉〉) |
41 | 39, 40 | eqtrd 2853 |
. . . . . . . . 9
⊢ (𝑛 = 𝑎 → 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉 = 〈𝑎, 𝑎, 〈“𝑤(𝑀‘𝑤)”〉〉) |
42 | 41 | oveq2d 7161 |
. . . . . . . 8
⊢ (𝑛 = 𝑎 → (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉) = (𝑣 splice 〈𝑎, 𝑎, 〈“𝑤(𝑀‘𝑤)”〉〉)) |
43 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑏 → 𝑤 = 𝑏) |
44 | | fveq2 6663 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑏 → (𝑀‘𝑤) = (𝑀‘𝑏)) |
45 | 43, 44 | s2eqd 14213 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑏 → 〈“𝑤(𝑀‘𝑤)”〉 = 〈“𝑏(𝑀‘𝑏)”〉) |
46 | 45 | oteq3d 4809 |
. . . . . . . . 9
⊢ (𝑤 = 𝑏 → 〈𝑎, 𝑎, 〈“𝑤(𝑀‘𝑤)”〉〉 = 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) |
47 | 46 | oveq2d 7161 |
. . . . . . . 8
⊢ (𝑤 = 𝑏 → (𝑣 splice 〈𝑎, 𝑎, 〈“𝑤(𝑀‘𝑤)”〉〉) = (𝑣 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) |
48 | 42, 47 | cbvmpov 7238 |
. . . . . . 7
⊢ (𝑛 ∈
(0...(♯‘𝑣)),
𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉)) = (𝑎 ∈ (0...(♯‘𝑣)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) |
49 | | fveq2 6663 |
. . . . . . . . 9
⊢ (𝑣 = 𝑢 → (♯‘𝑣) = (♯‘𝑢)) |
50 | 49 | oveq2d 7161 |
. . . . . . . 8
⊢ (𝑣 = 𝑢 → (0...(♯‘𝑣)) = (0...(♯‘𝑢))) |
51 | | eqidd 2819 |
. . . . . . . 8
⊢ (𝑣 = 𝑢 → (𝐼 × 2o) = (𝐼 × 2o)) |
52 | | oveq1 7152 |
. . . . . . . 8
⊢ (𝑣 = 𝑢 → (𝑣 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) = (𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) |
53 | 50, 51, 52 | mpoeq123dv 7218 |
. . . . . . 7
⊢ (𝑣 = 𝑢 → (𝑎 ∈ (0...(♯‘𝑣)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) = (𝑎 ∈ (0...(♯‘𝑢)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
54 | 48, 53 | syl5eq 2865 |
. . . . . 6
⊢ (𝑣 = 𝑢 → (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉)) = (𝑎 ∈ (0...(♯‘𝑢)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
55 | 54 | cbvmptv 5160 |
. . . . 5
⊢ (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) = (𝑢 ∈ 𝑊 ↦ (𝑎 ∈ (0...(♯‘𝑢)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
56 | 38, 55 | eqtri 2841 |
. . . 4
⊢ 𝑇 = (𝑢 ∈ 𝑊 ↦ (𝑎 ∈ (0...(♯‘𝑢)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
57 | 37, 56 | fvmptg 6759 |
. . 3
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∈ V) →
(𝑇‘𝑋) = (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
58 | 32, 57 | mpdan 683 |
. 2
⊢ (𝑋 ∈ 𝑊 → (𝑇‘𝑋) = (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
59 | 58 | feq1d 6492 |
. . 3
⊢ (𝑋 ∈ 𝑊 → ((𝑇‘𝑋):((0...(♯‘𝑋)) × (𝐼 × 2o))⟶𝑊 ↔ (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)):((0...(♯‘𝑋)) × (𝐼 × 2o))⟶𝑊)) |
60 | 21, 59 | mpbird 258 |
. 2
⊢ (𝑋 ∈ 𝑊 → (𝑇‘𝑋):((0...(♯‘𝑋)) × (𝐼 × 2o))⟶𝑊) |
61 | 58, 60 | jca 512 |
1
⊢ (𝑋 ∈ 𝑊 → ((𝑇‘𝑋) = (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∧ (𝑇‘𝑋):((0...(♯‘𝑋)) × (𝐼 × 2o))⟶𝑊)) |