Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . . . . . . . 10
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
2 | | fviss 6418 |
. . . . . . . . . 10
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ⊆ Word (𝐼 ×
2𝑜) |
3 | 1, 2 | eqsstri 3776 |
. . . . . . . . 9
⊢ 𝑊 ⊆ Word (𝐼 ×
2𝑜) |
4 | | simpl 474 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
𝑋 ∈ 𝑊) |
5 | 3, 4 | sseldi 3742 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
𝑋 ∈ Word (𝐼 ×
2𝑜)) |
6 | | simprr 813 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
𝑏 ∈ (𝐼 ×
2𝑜)) |
7 | | efgval2.m |
. . . . . . . . . . . 12
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
8 | 7 | efgmf 18326 |
. . . . . . . . . . 11
⊢ 𝑀:(𝐼 ×
2𝑜)⟶(𝐼 ×
2𝑜) |
9 | 8 | ffvelrni 6521 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (𝐼 × 2𝑜) →
(𝑀‘𝑏) ∈ (𝐼 ×
2𝑜)) |
10 | 9 | ad2antll 767 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑀‘𝑏) ∈ (𝐼 ×
2𝑜)) |
11 | 6, 10 | s2cld 13816 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
〈“𝑏(𝑀‘𝑏)”〉 ∈ Word (𝐼 ×
2𝑜)) |
12 | | splcl 13703 |
. . . . . . . 8
⊢ ((𝑋 ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑏(𝑀‘𝑏)”〉 ∈ Word (𝐼 × 2𝑜)) →
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) ∈ Word (𝐼 ×
2𝑜)) |
13 | 5, 11, 12 | syl2anc 696 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) ∈ Word (𝐼 ×
2𝑜)) |
14 | 1 | efgrcl 18328 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 ×
2𝑜))) |
15 | 14 | simprd 482 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑊 → 𝑊 = Word (𝐼 ×
2𝑜)) |
16 | 15 | adantr 472 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
𝑊 = Word (𝐼 ×
2𝑜)) |
17 | 13, 16 | eleqtrrd 2842 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) ∈ 𝑊) |
18 | 17 | ralrimivva 3109 |
. . . . 5
⊢ (𝑋 ∈ 𝑊 → ∀𝑎 ∈ (0...(♯‘𝑋))∀𝑏 ∈ (𝐼 × 2𝑜)(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) ∈ 𝑊) |
19 | | eqid 2760 |
. . . . . 6
⊢ (𝑎 ∈
(0...(♯‘𝑋)),
𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) = (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) |
20 | 19 | fmpt2 7405 |
. . . . 5
⊢
(∀𝑎 ∈
(0...(♯‘𝑋))∀𝑏 ∈ (𝐼 × 2𝑜)(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) ∈ 𝑊 ↔ (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)):((0...(♯‘𝑋)) × (𝐼 × 2𝑜))⟶𝑊) |
21 | 18, 20 | sylib 208 |
. . . 4
⊢ (𝑋 ∈ 𝑊 → (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)):((0...(♯‘𝑋)) × (𝐼 × 2𝑜))⟶𝑊) |
22 | | ovex 6841 |
. . . . 5
⊢
(0...(♯‘𝑋)) ∈ V |
23 | 14 | simpld 477 |
. . . . . 6
⊢ (𝑋 ∈ 𝑊 → 𝐼 ∈ V) |
24 | | 2on 7737 |
. . . . . 6
⊢
2𝑜 ∈ On |
25 | | xpexg 7125 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧
2𝑜 ∈ On) → (𝐼 × 2𝑜) ∈
V) |
26 | 23, 24, 25 | sylancl 697 |
. . . . 5
⊢ (𝑋 ∈ 𝑊 → (𝐼 × 2𝑜) ∈
V) |
27 | | xpexg 7125 |
. . . . 5
⊢
(((0...(♯‘𝑋)) ∈ V ∧ (𝐼 × 2𝑜) ∈ V)
→ ((0...(♯‘𝑋)) × (𝐼 × 2𝑜)) ∈
V) |
28 | 22, 26, 27 | sylancr 698 |
. . . 4
⊢ (𝑋 ∈ 𝑊 → ((0...(♯‘𝑋)) × (𝐼 × 2𝑜)) ∈
V) |
29 | | fvex 6362 |
. . . . . 6
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ∈ V |
30 | 1, 29 | eqeltri 2835 |
. . . . 5
⊢ 𝑊 ∈ V |
31 | 30 | a1i 11 |
. . . 4
⊢ (𝑋 ∈ 𝑊 → 𝑊 ∈ V) |
32 | | fex2 7286 |
. . . 4
⊢ (((𝑎 ∈
(0...(♯‘𝑋)),
𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)):((0...(♯‘𝑋)) × (𝐼 × 2𝑜))⟶𝑊 ∧ ((0...(♯‘𝑋)) × (𝐼 × 2𝑜)) ∈ V ∧
𝑊 ∈ V) → (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦ (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∈ V) |
33 | 21, 28, 31, 32 | syl3anc 1477 |
. . 3
⊢ (𝑋 ∈ 𝑊 → (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∈
V) |
34 | | fveq2 6352 |
. . . . . 6
⊢ (𝑢 = 𝑋 → (♯‘𝑢) = (♯‘𝑋)) |
35 | 34 | oveq2d 6829 |
. . . . 5
⊢ (𝑢 = 𝑋 → (0...(♯‘𝑢)) = (0...(♯‘𝑋))) |
36 | | eqidd 2761 |
. . . . 5
⊢ (𝑢 = 𝑋 → (𝐼 × 2𝑜) = (𝐼 ×
2𝑜)) |
37 | | oveq1 6820 |
. . . . 5
⊢ (𝑢 = 𝑋 → (𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) = (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) |
38 | 35, 36, 37 | mpt2eq123dv 6882 |
. . . 4
⊢ (𝑢 = 𝑋 → (𝑎 ∈ (0...(♯‘𝑢)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) = (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
39 | | efgval2.t |
. . . . 5
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
40 | | oteq1 4562 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑎 → 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉 = 〈𝑎, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉) |
41 | | oteq2 4563 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑎 → 〈𝑎, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉 = 〈𝑎, 𝑎, 〈“𝑤(𝑀‘𝑤)”〉〉) |
42 | 40, 41 | eqtrd 2794 |
. . . . . . . . 9
⊢ (𝑛 = 𝑎 → 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉 = 〈𝑎, 𝑎, 〈“𝑤(𝑀‘𝑤)”〉〉) |
43 | 42 | oveq2d 6829 |
. . . . . . . 8
⊢ (𝑛 = 𝑎 → (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉) = (𝑣 splice 〈𝑎, 𝑎, 〈“𝑤(𝑀‘𝑤)”〉〉)) |
44 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑏 → 𝑤 = 𝑏) |
45 | | fveq2 6352 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑏 → (𝑀‘𝑤) = (𝑀‘𝑏)) |
46 | 44, 45 | s2eqd 13808 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑏 → 〈“𝑤(𝑀‘𝑤)”〉 = 〈“𝑏(𝑀‘𝑏)”〉) |
47 | 46 | oteq3d 4567 |
. . . . . . . . 9
⊢ (𝑤 = 𝑏 → 〈𝑎, 𝑎, 〈“𝑤(𝑀‘𝑤)”〉〉 = 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) |
48 | 47 | oveq2d 6829 |
. . . . . . . 8
⊢ (𝑤 = 𝑏 → (𝑣 splice 〈𝑎, 𝑎, 〈“𝑤(𝑀‘𝑤)”〉〉) = (𝑣 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) |
49 | 43, 48 | cbvmpt2v 6900 |
. . . . . . 7
⊢ (𝑛 ∈
(0...(♯‘𝑣)),
𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉)) = (𝑎 ∈ (0...(♯‘𝑣)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) |
50 | | fveq2 6352 |
. . . . . . . . 9
⊢ (𝑣 = 𝑢 → (♯‘𝑣) = (♯‘𝑢)) |
51 | 50 | oveq2d 6829 |
. . . . . . . 8
⊢ (𝑣 = 𝑢 → (0...(♯‘𝑣)) = (0...(♯‘𝑢))) |
52 | | eqidd 2761 |
. . . . . . . 8
⊢ (𝑣 = 𝑢 → (𝐼 × 2𝑜) = (𝐼 ×
2𝑜)) |
53 | | oveq1 6820 |
. . . . . . . 8
⊢ (𝑣 = 𝑢 → (𝑣 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉) = (𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) |
54 | 51, 52, 53 | mpt2eq123dv 6882 |
. . . . . . 7
⊢ (𝑣 = 𝑢 → (𝑎 ∈ (0...(♯‘𝑣)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) = (𝑎 ∈ (0...(♯‘𝑢)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
55 | 49, 54 | syl5eq 2806 |
. . . . . 6
⊢ (𝑣 = 𝑢 → (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉)) = (𝑎 ∈ (0...(♯‘𝑢)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
56 | 55 | cbvmptv 4902 |
. . . . 5
⊢ (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) = (𝑢 ∈ 𝑊 ↦ (𝑎 ∈ (0...(♯‘𝑢)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
57 | 39, 56 | eqtri 2782 |
. . . 4
⊢ 𝑇 = (𝑢 ∈ 𝑊 ↦ (𝑎 ∈ (0...(♯‘𝑢)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑢 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
58 | 38, 57 | fvmptg 6442 |
. . 3
⊢ ((𝑋 ∈ 𝑊 ∧ (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∈ V) →
(𝑇‘𝑋) = (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
59 | 33, 58 | mpdan 705 |
. 2
⊢ (𝑋 ∈ 𝑊 → (𝑇‘𝑋) = (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉))) |
60 | 59 | feq1d 6191 |
. . 3
⊢ (𝑋 ∈ 𝑊 → ((𝑇‘𝑋):((0...(♯‘𝑋)) × (𝐼 ×
2𝑜))⟶𝑊 ↔ (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)):((0...(♯‘𝑋)) × (𝐼 × 2𝑜))⟶𝑊)) |
61 | 21, 60 | mpbird 247 |
. 2
⊢ (𝑋 ∈ 𝑊 → (𝑇‘𝑋):((0...(♯‘𝑋)) × (𝐼 ×
2𝑜))⟶𝑊) |
62 | 59, 61 | jca 555 |
1
⊢ (𝑋 ∈ 𝑊 → ((𝑇‘𝑋) = (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∧ (𝑇‘𝑋):((0...(♯‘𝑋)) × (𝐼 ×
2𝑜))⟶𝑊)) |