Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . . . . . . . 10
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
2 | | fviss 6166 |
. . . . . . . . . 10
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ⊆ Word (𝐼 ×
2𝑜) |
3 | 1, 2 | eqsstri 3598 |
. . . . . . . . 9
⊢ 𝑊 ⊆ Word (𝐼 ×
2𝑜) |
4 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(#‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
𝑋 ∈ 𝑊) |
5 | 3, 4 | sseldi 3566 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(#‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
𝑋 ∈ Word (𝐼 ×
2𝑜)) |
6 | | simprr 792 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(#‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
𝑏 ∈ (𝐼 ×
2𝑜)) |
7 | | efgval2.m |
. . . . . . . . . . . 12
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
8 | 7 | efgmf 17949 |
. . . . . . . . . . 11
⊢ 𝑀:(𝐼 ×
2𝑜)⟶(𝐼 ×
2𝑜) |
9 | 8 | ffvelrni 6266 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (𝐼 × 2𝑜) →
(𝑀‘𝑏) ∈ (𝐼 ×
2𝑜)) |
10 | 9 | ad2antll 761 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(#‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑀‘𝑏) ∈ (𝐼 ×
2𝑜)) |
11 | 6, 10 | s2cld 13466 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(#‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
〈“𝑏(𝑀‘𝑏)”〉 ∈ Word (𝐼 ×
2𝑜)) |
12 | | splcl 13354 |
. . . . . . . 8
⊢ ((𝑋 ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑏(𝑀‘𝑏)”〉 ∈ Word (𝐼 × 2𝑜)) →
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) ∈ Word (𝐼 ×
2𝑜)) |
13 | 5, 11, 12 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(#‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) ∈ Word (𝐼 ×
2𝑜)) |
14 | 1 | efgrcl 17951 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 ×
2𝑜))) |
15 | 14 | simprd 478 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑊 → 𝑊 = Word (𝐼 ×
2𝑜)) |
16 | 15 | adantr 480 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(#‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
𝑊 = Word (𝐼 ×
2𝑜)) |
17 | 13, 16 | eleqtrrd 2691 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(#‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) ∈ 𝑊) |
18 | 17 | ralrimivva 2954 |
. . . . 5
⊢ (𝑋 ∈ 𝑊 → ∀𝑎 ∈ (0...(#‘𝑋))∀𝑏 ∈ (𝐼 × 2𝑜)(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) ∈ 𝑊) |
19 | | eqid 2610 |
. . . . . 6
⊢ (𝑎 ∈ (0...(#‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) = (𝑎 ∈ (0...(#‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) |
20 | 19 | fmpt2 7126 |
. . . . 5
⊢
(∀𝑎 ∈
(0...(#‘𝑋))∀𝑏 ∈ (𝐼 × 2𝑜)(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) ∈ 𝑊 ↔ (𝑎 ∈ (0...(#‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)):((0...(#‘𝑋)) × (𝐼 ×
2𝑜))⟶𝑊) |
21 | 18, 20 | sylib 207 |
. . . 4
⊢ (𝑋 ∈ 𝑊 → (𝑎 ∈ (0...(#‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)):((0...(#‘𝑋)) × (𝐼 ×
2𝑜))⟶𝑊) |
22 | | ovex 6577 |
. . . . 5
⊢
(0...(#‘𝑋))
∈ V |
23 | 14 | simpld 474 |
. . . . . 6
⊢ (𝑋 ∈ 𝑊 → 𝐼 ∈ V) |
24 | | 2on 7455 |
. . . . . 6
⊢
2𝑜 ∈ On |
25 | | xpexg 6858 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧
2𝑜 ∈ On) → (𝐼 × 2𝑜) ∈
V) |
26 | 23, 24, 25 | sylancl 693 |
. . . . 5
⊢ (𝑋 ∈ 𝑊 → (𝐼 × 2𝑜) ∈
V) |
27 | | xpexg 6858 |
. . . . 5
⊢
(((0...(#‘𝑋))
∈ V ∧ (𝐼 ×
2𝑜) ∈ V) → ((0...(#‘𝑋)) × (𝐼 × 2𝑜)) ∈
V) |
28 | 22, 26, 27 | sylancr 694 |
. . . 4
⊢ (𝑋 ∈ 𝑊 → ((0...(#‘𝑋)) × (𝐼 × 2𝑜)) ∈
V) |
29 | | fvex 6113 |
. . . . . 6
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ∈ V |
30 | 1, 29 | eqeltri 2684 |
. . . . 5
⊢ 𝑊 ∈ V |
31 | 30 | a1i 11 |
. . . 4
⊢ (𝑋 ∈ 𝑊 → 𝑊 ∈ V) |
32 | | fex2 7014 |
. . . 4
⊢ (((𝑎 ∈ (0...(#‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)):((0...(#‘𝑋)) × (𝐼 ×
2𝑜))⟶𝑊 ∧ ((0...(#‘𝑋)) × (𝐼 × 2𝑜)) ∈ V
∧ 𝑊 ∈ V) →
(𝑎 ∈
(0...(#‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∈
V) |
33 | 21, 28, 31, 32 | syl3anc 1318 |
. . 3
⊢ (𝑋 ∈ 𝑊 → (𝑎 ∈ (0...(#‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∈
V) |
34 | | fveq2 6103 |
. . . . . 6
⊢ (𝑢 = 𝑋 → (#‘𝑢) = (#‘𝑋)) |
35 | 34 | oveq2d 6565 |
. . . . 5
⊢ (𝑢 = 𝑋 → (0...(#‘𝑢)) = (0...(#‘𝑋))) |
36 | | eqidd 2611 |
. . . . 5
⊢ (𝑢 = 𝑋 → (𝐼 × 2𝑜) = (𝐼 ×
2𝑜)) |
37 | | oveq1 6556 |
. . . . 5
⊢ (𝑢 = 𝑋 → (𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) = (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) |
38 | 35, 36, 37 | mpt2eq123dv 6615 |
. . . 4
⊢ (𝑢 = 𝑋 → (𝑎 ∈ (0...(#‘𝑢)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) = (𝑎 ∈ (0...(#‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
39 | | efgval2.t |
. . . . 5
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
40 | | oteq1 4349 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑎 → 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉 = 〈𝑎, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉) |
41 | | oteq2 4350 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑎 → 〈𝑎, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉 = 〈𝑎, 𝑎, 〈“𝑤(𝑀‘𝑤)”〉〉) |
42 | 40, 41 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝑛 = 𝑎 → 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉 = 〈𝑎, 𝑎, 〈“𝑤(𝑀‘𝑤)”〉〉) |
43 | 42 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑛 = 𝑎 → (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉) = (𝑣 splice 〈𝑎, 𝑎, 〈“𝑤(𝑀‘𝑤)”〉〉)) |
44 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑏 → 𝑤 = 𝑏) |
45 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑏 → (𝑀‘𝑤) = (𝑀‘𝑏)) |
46 | 44, 45 | s2eqd 13459 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑏 → 〈“𝑤(𝑀‘𝑤)”〉 = 〈“𝑏(𝑀‘𝑏)”〉) |
47 | 46 | oteq3d 4354 |
. . . . . . . . 9
⊢ (𝑤 = 𝑏 → 〈𝑎, 𝑎, 〈“𝑤(𝑀‘𝑤)”〉〉 = 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) |
48 | 47 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑤 = 𝑏 → (𝑣 splice 〈𝑎, 𝑎, 〈“𝑤(𝑀‘𝑤)”〉〉) = (𝑣 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) |
49 | 43, 48 | cbvmpt2v 6633 |
. . . . . . 7
⊢ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉)) = (𝑎 ∈ (0...(#‘𝑣)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) |
50 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑣 = 𝑢 → (#‘𝑣) = (#‘𝑢)) |
51 | 50 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑣 = 𝑢 → (0...(#‘𝑣)) = (0...(#‘𝑢))) |
52 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝑣 = 𝑢 → (𝐼 × 2𝑜) = (𝐼 ×
2𝑜)) |
53 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑣 = 𝑢 → (𝑣 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) = (𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) |
54 | 51, 52, 53 | mpt2eq123dv 6615 |
. . . . . . 7
⊢ (𝑣 = 𝑢 → (𝑎 ∈ (0...(#‘𝑣)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) = (𝑎 ∈ (0...(#‘𝑢)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
55 | 49, 54 | syl5eq 2656 |
. . . . . 6
⊢ (𝑣 = 𝑢 → (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉)) = (𝑎 ∈ (0...(#‘𝑢)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
56 | 55 | cbvmptv 4678 |
. . . . 5
⊢ (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) = (𝑢 ∈ 𝑊 ↦ (𝑎 ∈ (0...(#‘𝑢)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
57 | 39, 56 | eqtri 2632 |
. . . 4
⊢ 𝑇 = (𝑢 ∈ 𝑊 ↦ (𝑎 ∈ (0...(#‘𝑢)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
58 | 38, 57 | fvmptg 6189 |
. . 3
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(#‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∈ V) →
(𝑇‘𝑋) = (𝑎 ∈ (0...(#‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
59 | 33, 58 | mpdan 699 |
. 2
⊢ (𝑋 ∈ 𝑊 → (𝑇‘𝑋) = (𝑎 ∈ (0...(#‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
60 | 59 | feq1d 5943 |
. . 3
⊢ (𝑋 ∈ 𝑊 → ((𝑇‘𝑋):((0...(#‘𝑋)) × (𝐼 ×
2𝑜))⟶𝑊 ↔ (𝑎 ∈ (0...(#‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)):((0...(#‘𝑋)) × (𝐼 ×
2𝑜))⟶𝑊)) |
61 | 21, 60 | mpbird 246 |
. 2
⊢ (𝑋 ∈ 𝑊 → (𝑇‘𝑋):((0...(#‘𝑋)) × (𝐼 ×
2𝑜))⟶𝑊) |
62 | 59, 61 | jca 553 |
1
⊢ (𝑋 ∈ 𝑊 → ((𝑇‘𝑋) = (𝑎 ∈ (0...(#‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∧ (𝑇‘𝑋):((0...(#‘𝑋)) × (𝐼 ×
2𝑜))⟶𝑊)) |