Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . . . . . . . 10
β’ π = ( I βWord (πΌ Γ
2o)) |
2 | | fviss 6954 |
. . . . . . . . . 10
β’ ( I
βWord (πΌ Γ
2o)) β Word (πΌ Γ 2o) |
3 | 1, 2 | eqsstri 4012 |
. . . . . . . . 9
β’ π β Word (πΌ Γ 2o) |
4 | | simpl 483 |
. . . . . . . . 9
β’ ((π β π β§ (π β (0...(β―βπ)) β§ π β (πΌ Γ 2o))) β π β π) |
5 | 3, 4 | sselid 3976 |
. . . . . . . 8
β’ ((π β π β§ (π β (0...(β―βπ)) β§ π β (πΌ Γ 2o))) β π β Word (πΌ Γ 2o)) |
6 | | simprr 771 |
. . . . . . . . 9
β’ ((π β π β§ (π β (0...(β―βπ)) β§ π β (πΌ Γ 2o))) β π β (πΌ Γ 2o)) |
7 | | efgval2.m |
. . . . . . . . . . . 12
β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
8 | 7 | efgmf 19545 |
. . . . . . . . . . 11
β’ π:(πΌ Γ 2o)βΆ(πΌ Γ
2o) |
9 | 8 | ffvelcdmi 7070 |
. . . . . . . . . 10
β’ (π β (πΌ Γ 2o) β (πβπ) β (πΌ Γ 2o)) |
10 | 9 | ad2antll 727 |
. . . . . . . . 9
β’ ((π β π β§ (π β (0...(β―βπ)) β§ π β (πΌ Γ 2o))) β (πβπ) β (πΌ Γ 2o)) |
11 | 6, 10 | s2cld 14804 |
. . . . . . . 8
β’ ((π β π β§ (π β (0...(β―βπ)) β§ π β (πΌ Γ 2o))) β
β¨βπ(πβπ)ββ© β Word (πΌ Γ 2o)) |
12 | | splcl 14684 |
. . . . . . . 8
β’ ((π β Word (πΌ Γ 2o) β§
β¨βπ(πβπ)ββ© β Word (πΌ Γ 2o)) β (π splice β¨π, π, β¨βπ(πβπ)ββ©β©) β Word (πΌ Γ
2o)) |
13 | 5, 11, 12 | syl2anc 584 |
. . . . . . 7
β’ ((π β π β§ (π β (0...(β―βπ)) β§ π β (πΌ Γ 2o))) β (π splice β¨π, π, β¨βπ(πβπ)ββ©β©) β Word (πΌ Γ
2o)) |
14 | 1 | efgrcl 19547 |
. . . . . . . . 9
β’ (π β π β (πΌ β V β§ π = Word (πΌ Γ 2o))) |
15 | 14 | simprd 496 |
. . . . . . . 8
β’ (π β π β π = Word (πΌ Γ 2o)) |
16 | 15 | adantr 481 |
. . . . . . 7
β’ ((π β π β§ (π β (0...(β―βπ)) β§ π β (πΌ Γ 2o))) β π = Word (πΌ Γ 2o)) |
17 | 13, 16 | eleqtrrd 2835 |
. . . . . 6
β’ ((π β π β§ (π β (0...(β―βπ)) β§ π β (πΌ Γ 2o))) β (π splice β¨π, π, β¨βπ(πβπ)ββ©β©) β π) |
18 | 17 | ralrimivva 3199 |
. . . . 5
β’ (π β π β βπ β (0...(β―βπ))βπ β (πΌ Γ 2o)(π splice β¨π, π, β¨βπ(πβπ)ββ©β©) β π) |
19 | | eqid 2731 |
. . . . . 6
β’ (π β
(0...(β―βπ)),
π β (πΌ Γ 2o) β¦ (π splice β¨π, π, β¨βπ(πβπ)ββ©β©)) = (π β (0...(β―βπ)), π β (πΌ Γ 2o) β¦ (π splice β¨π, π, β¨βπ(πβπ)ββ©β©)) |
20 | 19 | fmpo 8036 |
. . . . 5
β’
(βπ β
(0...(β―βπ))βπ β (πΌ Γ 2o)(π splice β¨π, π, β¨βπ(πβπ)ββ©β©) β π β (π β (0...(β―βπ)), π β (πΌ Γ 2o) β¦ (π splice β¨π, π, β¨βπ(πβπ)ββ©β©)):((0...(β―βπ)) Γ (πΌ Γ 2o))βΆπ) |
21 | 18, 20 | sylib 217 |
. . . 4
β’ (π β π β (π β (0...(β―βπ)), π β (πΌ Γ 2o) β¦ (π splice β¨π, π, β¨βπ(πβπ)ββ©β©)):((0...(β―βπ)) Γ (πΌ Γ 2o))βΆπ) |
22 | | ovex 7426 |
. . . . 5
β’
(0...(β―βπ)) β V |
23 | 14 | simpld 495 |
. . . . . 6
β’ (π β π β πΌ β V) |
24 | | 2on 8462 |
. . . . . 6
β’
2o β On |
25 | | xpexg 7720 |
. . . . . 6
β’ ((πΌ β V β§ 2o
β On) β (πΌ
Γ 2o) β V) |
26 | 23, 24, 25 | sylancl 586 |
. . . . 5
β’ (π β π β (πΌ Γ 2o) β
V) |
27 | | xpexg 7720 |
. . . . 5
β’
(((0...(β―βπ)) β V β§ (πΌ Γ 2o) β V) β
((0...(β―βπ))
Γ (πΌ Γ
2o)) β V) |
28 | 22, 26, 27 | sylancr 587 |
. . . 4
β’ (π β π β ((0...(β―βπ)) Γ (πΌ Γ 2o)) β
V) |
29 | 21, 28 | fexd 7213 |
. . 3
β’ (π β π β (π β (0...(β―βπ)), π β (πΌ Γ 2o) β¦ (π splice β¨π, π, β¨βπ(πβπ)ββ©β©)) β
V) |
30 | | fveq2 6878 |
. . . . . 6
β’ (π’ = π β (β―βπ’) = (β―βπ)) |
31 | 30 | oveq2d 7409 |
. . . . 5
β’ (π’ = π β (0...(β―βπ’)) = (0...(β―βπ))) |
32 | | eqidd 2732 |
. . . . 5
β’ (π’ = π β (πΌ Γ 2o) = (πΌ Γ 2o)) |
33 | | oveq1 7400 |
. . . . 5
β’ (π’ = π β (π’ splice β¨π, π, β¨βπ(πβπ)ββ©β©) = (π splice β¨π, π, β¨βπ(πβπ)ββ©β©)) |
34 | 31, 32, 33 | mpoeq123dv 7468 |
. . . 4
β’ (π’ = π β (π β (0...(β―βπ’)), π β (πΌ Γ 2o) β¦ (π’ splice β¨π, π, β¨βπ(πβπ)ββ©β©)) = (π β (0...(β―βπ)), π β (πΌ Γ 2o) β¦ (π splice β¨π, π, β¨βπ(πβπ)ββ©β©))) |
35 | | efgval2.t |
. . . . 5
β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) |
36 | | oteq1 4875 |
. . . . . . . . . 10
β’ (π = π β β¨π, π, β¨βπ€(πβπ€)ββ©β© = β¨π, π, β¨βπ€(πβπ€)ββ©β©) |
37 | | oteq2 4876 |
. . . . . . . . . 10
β’ (π = π β β¨π, π, β¨βπ€(πβπ€)ββ©β© = β¨π, π, β¨βπ€(πβπ€)ββ©β©) |
38 | 36, 37 | eqtrd 2771 |
. . . . . . . . 9
β’ (π = π β β¨π, π, β¨βπ€(πβπ€)ββ©β© = β¨π, π, β¨βπ€(πβπ€)ββ©β©) |
39 | 38 | oveq2d 7409 |
. . . . . . . 8
β’ (π = π β (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©) = (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©)) |
40 | | id 22 |
. . . . . . . . . . 11
β’ (π€ = π β π€ = π) |
41 | | fveq2 6878 |
. . . . . . . . . . 11
β’ (π€ = π β (πβπ€) = (πβπ)) |
42 | 40, 41 | s2eqd 14796 |
. . . . . . . . . 10
β’ (π€ = π β β¨βπ€(πβπ€)ββ© = β¨βπ(πβπ)ββ©) |
43 | 42 | oteq3d 4880 |
. . . . . . . . 9
β’ (π€ = π β β¨π, π, β¨βπ€(πβπ€)ββ©β© = β¨π, π, β¨βπ(πβπ)ββ©β©) |
44 | 43 | oveq2d 7409 |
. . . . . . . 8
β’ (π€ = π β (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©) = (π£ splice β¨π, π, β¨βπ(πβπ)ββ©β©)) |
45 | 39, 44 | cbvmpov 7488 |
. . . . . . 7
β’ (π β
(0...(β―βπ£)),
π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©)) = (π β (0...(β―βπ£)), π β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ(πβπ)ββ©β©)) |
46 | | fveq2 6878 |
. . . . . . . . 9
β’ (π£ = π’ β (β―βπ£) = (β―βπ’)) |
47 | 46 | oveq2d 7409 |
. . . . . . . 8
β’ (π£ = π’ β (0...(β―βπ£)) = (0...(β―βπ’))) |
48 | | eqidd 2732 |
. . . . . . . 8
β’ (π£ = π’ β (πΌ Γ 2o) = (πΌ Γ 2o)) |
49 | | oveq1 7400 |
. . . . . . . 8
β’ (π£ = π’ β (π£ splice β¨π, π, β¨βπ(πβπ)ββ©β©) = (π’ splice β¨π, π, β¨βπ(πβπ)ββ©β©)) |
50 | 47, 48, 49 | mpoeq123dv 7468 |
. . . . . . 7
β’ (π£ = π’ β (π β (0...(β―βπ£)), π β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ(πβπ)ββ©β©)) = (π β (0...(β―βπ’)), π β (πΌ Γ 2o) β¦ (π’ splice β¨π, π, β¨βπ(πβπ)ββ©β©))) |
51 | 45, 50 | eqtrid 2783 |
. . . . . 6
β’ (π£ = π’ β (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©)) = (π β (0...(β―βπ’)), π β (πΌ Γ 2o) β¦ (π’ splice β¨π, π, β¨βπ(πβπ)ββ©β©))) |
52 | 51 | cbvmptv 5254 |
. . . . 5
β’ (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) = (π’ β π β¦ (π β (0...(β―βπ’)), π β (πΌ Γ 2o) β¦ (π’ splice β¨π, π, β¨βπ(πβπ)ββ©β©))) |
53 | 35, 52 | eqtri 2759 |
. . . 4
β’ π = (π’ β π β¦ (π β (0...(β―βπ’)), π β (πΌ Γ 2o) β¦ (π’ splice β¨π, π, β¨βπ(πβπ)ββ©β©))) |
54 | 34, 53 | fvmptg 6982 |
. . 3
β’ ((π β π β§ (π β (0...(β―βπ)), π β (πΌ Γ 2o) β¦ (π splice β¨π, π, β¨βπ(πβπ)ββ©β©)) β V) β
(πβπ) = (π β (0...(β―βπ)), π β (πΌ Γ 2o) β¦ (π splice β¨π, π, β¨βπ(πβπ)ββ©β©))) |
55 | 29, 54 | mpdan 685 |
. 2
β’ (π β π β (πβπ) = (π β (0...(β―βπ)), π β (πΌ Γ 2o) β¦ (π splice β¨π, π, β¨βπ(πβπ)ββ©β©))) |
56 | 55 | feq1d 6689 |
. . 3
β’ (π β π β ((πβπ):((0...(β―βπ)) Γ (πΌ Γ 2o))βΆπ β (π β (0...(β―βπ)), π β (πΌ Γ 2o) β¦ (π splice β¨π, π, β¨βπ(πβπ)ββ©β©)):((0...(β―βπ)) Γ (πΌ Γ 2o))βΆπ)) |
57 | 21, 56 | mpbird 256 |
. 2
β’ (π β π β (πβπ):((0...(β―βπ)) Γ (πΌ Γ 2o))βΆπ) |
58 | 55, 57 | jca 512 |
1
β’ (π β π β ((πβπ) = (π β (0...(β―βπ)), π β (πΌ Γ 2o) β¦ (π splice β¨π, π, β¨βπ(πβπ)ββ©β©)) β§ (πβπ):((0...(β―βπ)) Γ (πΌ Γ 2o))βΆπ)) |