Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . 3
β’ π = ( I βWord (πΌ Γ
2o)) |
2 | | efgval.r |
. . 3
β’ βΌ = (
~FG βπΌ) |
3 | 1, 2 | efgval 19626 |
. 2
β’ βΌ =
β© {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))} |
4 | | efgval2.m |
. . . . . . . . . . 11
β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
5 | | efgval2.t |
. . . . . . . . . . 11
β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) |
6 | 1, 2, 4, 5 | efgtf 19631 |
. . . . . . . . . 10
β’ (π₯ β π β ((πβπ₯) = (π β (0...(β―βπ₯)), π’ β (πΌ Γ 2o) β¦ (π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©)) β§ (πβπ₯):((0...(β―βπ₯)) Γ (πΌ Γ 2o))βΆπ)) |
7 | 6 | simpld 493 |
. . . . . . . . 9
β’ (π₯ β π β (πβπ₯) = (π β (0...(β―βπ₯)), π’ β (πΌ Γ 2o) β¦ (π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©))) |
8 | 7 | rneqd 5936 |
. . . . . . . 8
β’ (π₯ β π β ran (πβπ₯) = ran (π β (0...(β―βπ₯)), π’ β (πΌ Γ 2o) β¦ (π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©))) |
9 | 8 | sseq1d 4012 |
. . . . . . 7
β’ (π₯ β π β (ran (πβπ₯) β [π₯]π β ran (π β (0...(β―βπ₯)), π’ β (πΌ Γ 2o) β¦ (π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©)) β [π₯]π)) |
10 | | dfss3 3969 |
. . . . . . . 8
β’ (ran
(π β
(0...(β―βπ₯)),
π’ β (πΌ Γ 2o) β¦ (π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©)) β [π₯]π β βπ β ran (π β (0...(β―βπ₯)), π’ β (πΌ Γ 2o) β¦ (π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©))π β [π₯]π) |
11 | | ovex 7444 |
. . . . . . . . . . 11
β’ (π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©) β
V |
12 | 11 | rgen2w 3064 |
. . . . . . . . . 10
β’
βπ β
(0...(β―βπ₯))βπ’ β (πΌ Γ 2o)(π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©) β
V |
13 | | eqid 2730 |
. . . . . . . . . . 11
β’ (π β
(0...(β―βπ₯)),
π’ β (πΌ Γ 2o) β¦ (π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©)) = (π β (0...(β―βπ₯)), π’ β (πΌ Γ 2o) β¦ (π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©)) |
14 | | vex 3476 |
. . . . . . . . . . . . 13
β’ π β V |
15 | | vex 3476 |
. . . . . . . . . . . . 13
β’ π₯ β V |
16 | 14, 15 | elec 8749 |
. . . . . . . . . . . 12
β’ (π β [π₯]π β π₯ππ) |
17 | | breq2 5151 |
. . . . . . . . . . . 12
β’ (π = (π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©) β (π₯ππ β π₯π(π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©))) |
18 | 16, 17 | bitrid 282 |
. . . . . . . . . . 11
β’ (π = (π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©) β (π β [π₯]π β π₯π(π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©))) |
19 | 13, 18 | ralrnmpo 7549 |
. . . . . . . . . 10
β’
(βπ β
(0...(β―βπ₯))βπ’ β (πΌ Γ 2o)(π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©) β V β
(βπ β ran
(π β
(0...(β―βπ₯)),
π’ β (πΌ Γ 2o) β¦ (π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©))π β [π₯]π β βπ β (0...(β―βπ₯))βπ’ β (πΌ Γ 2o)π₯π(π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©))) |
20 | 12, 19 | ax-mp 5 |
. . . . . . . . 9
β’
(βπ β
ran (π β
(0...(β―βπ₯)),
π’ β (πΌ Γ 2o) β¦ (π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©))π β [π₯]π β βπ β (0...(β―βπ₯))βπ’ β (πΌ Γ 2o)π₯π(π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©)) |
21 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π’ = β¨π, πβ© β π’ = β¨π, πβ©) |
22 | | fveq2 6890 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = β¨π, πβ© β (πβπ’) = (πββ¨π, πβ©)) |
23 | | df-ov 7414 |
. . . . . . . . . . . . . . . . 17
β’ (πππ) = (πββ¨π, πβ©) |
24 | 22, 23 | eqtr4di 2788 |
. . . . . . . . . . . . . . . 16
β’ (π’ = β¨π, πβ© β (πβπ’) = (πππ)) |
25 | 21, 24 | s2eqd 14818 |
. . . . . . . . . . . . . . 15
β’ (π’ = β¨π, πβ© β β¨βπ’(πβπ’)ββ© = β¨ββ¨π, πβ©(πππ)ββ©) |
26 | 25 | oteq3d 4886 |
. . . . . . . . . . . . . 14
β’ (π’ = β¨π, πβ© β β¨π, π, β¨βπ’(πβπ’)ββ©β© = β¨π, π, β¨ββ¨π, πβ©(πππ)ββ©β©) |
27 | 26 | oveq2d 7427 |
. . . . . . . . . . . . 13
β’ (π’ = β¨π, πβ© β (π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©) = (π₯ splice β¨π, π, β¨ββ¨π, πβ©(πππ)ββ©β©)) |
28 | 27 | breq2d 5159 |
. . . . . . . . . . . 12
β’ (π’ = β¨π, πβ© β (π₯π(π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©) β π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©(πππ)ββ©β©))) |
29 | 28 | ralxp 5840 |
. . . . . . . . . . 11
β’
(βπ’ β
(πΌ Γ
2o)π₯π(π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©) β βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©(πππ)ββ©β©)) |
30 | | eqidd 2731 |
. . . . . . . . . . . . . . . . 17
β’ ((π β πΌ β§ π β 2o) β β¨π, πβ© = β¨π, πβ©) |
31 | 4 | efgmval 19621 |
. . . . . . . . . . . . . . . . 17
β’ ((π β πΌ β§ π β 2o) β (πππ) = β¨π, (1o β π)β©) |
32 | 30, 31 | s2eqd 14818 |
. . . . . . . . . . . . . . . 16
β’ ((π β πΌ β§ π β 2o) β
β¨ββ¨π, πβ©(πππ)ββ© = β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©) |
33 | 32 | oteq3d 4886 |
. . . . . . . . . . . . . . 15
β’ ((π β πΌ β§ π β 2o) β β¨π, π, β¨ββ¨π, πβ©(πππ)ββ©β© = β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) |
34 | 33 | oveq2d 7427 |
. . . . . . . . . . . . . 14
β’ ((π β πΌ β§ π β 2o) β (π₯ splice β¨π, π, β¨ββ¨π, πβ©(πππ)ββ©β©) = (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)) |
35 | 34 | breq2d 5159 |
. . . . . . . . . . . . 13
β’ ((π β πΌ β§ π β 2o) β (π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©(πππ)ββ©β©) β π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))) |
36 | 35 | ralbidva 3173 |
. . . . . . . . . . . 12
β’ (π β πΌ β (βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©(πππ)ββ©β©) β βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))) |
37 | 36 | ralbiia 3089 |
. . . . . . . . . . 11
β’
(βπ β
πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©(πππ)ββ©β©) β βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)) |
38 | 29, 37 | bitri 274 |
. . . . . . . . . 10
β’
(βπ’ β
(πΌ Γ
2o)π₯π(π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©) β βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)) |
39 | 38 | ralbii 3091 |
. . . . . . . . 9
β’
(βπ β
(0...(β―βπ₯))βπ’ β (πΌ Γ 2o)π₯π(π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©) β βπ β
(0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)) |
40 | 20, 39 | bitri 274 |
. . . . . . . 8
β’
(βπ β
ran (π β
(0...(β―βπ₯)),
π’ β (πΌ Γ 2o) β¦ (π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©))π β [π₯]π β βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)) |
41 | 10, 40 | bitri 274 |
. . . . . . 7
β’ (ran
(π β
(0...(β―βπ₯)),
π’ β (πΌ Γ 2o) β¦ (π₯ splice β¨π, π, β¨βπ’(πβπ’)ββ©β©)) β [π₯]π β βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)) |
42 | 9, 41 | bitrdi 286 |
. . . . . 6
β’ (π₯ β π β (ran (πβπ₯) β [π₯]π β βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))) |
43 | 42 | ralbiia 3089 |
. . . . 5
β’
(βπ₯ β
π ran (πβπ₯) β [π₯]π β βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)) |
44 | 43 | anbi2i 621 |
. . . 4
β’ ((π Er π β§ βπ₯ β π ran (πβπ₯) β [π₯]π) β (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))) |
45 | 44 | abbii 2800 |
. . 3
β’ {π β£ (π Er π β§ βπ₯ β π ran (πβπ₯) β [π₯]π)} = {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))} |
46 | 45 | inteqi 4953 |
. 2
β’ β© {π
β£ (π Er π β§ βπ₯ β π ran (πβπ₯) β [π₯]π)} = β© {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))} |
47 | 3, 46 | eqtr4i 2761 |
1
β’ βΌ =
β© {π β£ (π Er π β§ βπ₯ β π ran (πβπ₯) β [π₯]π)} |