Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . . 4
β’
(VtxβπΊ) =
(VtxβπΊ) |
2 | 1 | wlkp 28862 |
. . 3
β’ (πΉ(WalksβπΊ)π β π:(0...(β―βπΉ))βΆ(VtxβπΊ)) |
3 | | oveq2 7413 |
. . . . . . . . . . . . 13
β’
((β―βπΉ) =
1 β (0...(β―βπΉ)) = (0...1)) |
4 | | 1e0p1 12715 |
. . . . . . . . . . . . . . 15
β’ 1 = (0 +
1) |
5 | 4 | oveq2i 7416 |
. . . . . . . . . . . . . 14
β’ (0...1) =
(0...(0 + 1)) |
6 | | 0z 12565 |
. . . . . . . . . . . . . . 15
β’ 0 β
β€ |
7 | | fzpr 13552 |
. . . . . . . . . . . . . . 15
β’ (0 β
β€ β (0...(0 + 1)) = {0, (0 + 1)}) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ (0...(0 +
1)) = {0, (0 + 1)} |
9 | | 0p1e1 12330 |
. . . . . . . . . . . . . . 15
β’ (0 + 1) =
1 |
10 | 9 | preq2i 4740 |
. . . . . . . . . . . . . 14
β’ {0, (0 +
1)} = {0, 1} |
11 | 5, 8, 10 | 3eqtri 2764 |
. . . . . . . . . . . . 13
β’ (0...1) =
{0, 1} |
12 | 3, 11 | eqtrdi 2788 |
. . . . . . . . . . . 12
β’
((β―βπΉ) =
1 β (0...(β―βπΉ)) = {0, 1}) |
13 | 12 | feq2d 6700 |
. . . . . . . . . . 11
β’
((β―βπΉ) =
1 β (π:(0...(β―βπΉ))βΆ(VtxβπΊ) β π:{0, 1}βΆ(VtxβπΊ))) |
14 | 13 | adantr 481 |
. . . . . . . . . 10
β’
(((β―βπΉ)
= 1 β§ ((πβ0) =
π΄ β§ (πβ(β―βπΉ)) = π΅)) β (π:(0...(β―βπΉ))βΆ(VtxβπΊ) β π:{0, 1}βΆ(VtxβπΊ))) |
15 | | simpl 483 |
. . . . . . . . . . . . 13
β’ (((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β (πβ0) = π΄) |
16 | | simpr 485 |
. . . . . . . . . . . . 13
β’ (((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β (πβ(β―βπΉ)) = π΅) |
17 | 15, 16 | neeq12d 3002 |
. . . . . . . . . . . 12
β’ (((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β ((πβ0) β (πβ(β―βπΉ)) β π΄ β π΅)) |
18 | 17 | bicomd 222 |
. . . . . . . . . . 11
β’ (((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β (π΄ β π΅ β (πβ0) β (πβ(β―βπΉ)))) |
19 | | fveq2 6888 |
. . . . . . . . . . . 12
β’
((β―βπΉ) =
1 β (πβ(β―βπΉ)) = (πβ1)) |
20 | 19 | neeq2d 3001 |
. . . . . . . . . . 11
β’
((β―βπΉ) =
1 β ((πβ0) β
(πβ(β―βπΉ)) β (πβ0) β (πβ1))) |
21 | 18, 20 | sylan9bbr 511 |
. . . . . . . . . 10
β’
(((β―βπΉ)
= 1 β§ ((πβ0) =
π΄ β§ (πβ(β―βπΉ)) = π΅)) β (π΄ β π΅ β (πβ0) β (πβ1))) |
22 | 14, 21 | anbi12d 631 |
. . . . . . . . 9
β’
(((β―βπΉ)
= 1 β§ ((πβ0) =
π΄ β§ (πβ(β―βπΉ)) = π΅)) β ((π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ π΄ β π΅) β (π:{0, 1}βΆ(VtxβπΊ) β§ (πβ0) β (πβ1)))) |
23 | | 1z 12588 |
. . . . . . . . . . . 12
β’ 1 β
β€ |
24 | | fpr2g 7209 |
. . . . . . . . . . . 12
β’ ((0
β β€ β§ 1 β β€) β (π:{0, 1}βΆ(VtxβπΊ) β ((πβ0) β (VtxβπΊ) β§ (πβ1) β (VtxβπΊ) β§ π = {β¨0, (πβ0)β©, β¨1, (πβ1)β©}))) |
25 | 6, 23, 24 | mp2an 690 |
. . . . . . . . . . 11
β’ (π:{0, 1}βΆ(VtxβπΊ) β ((πβ0) β (VtxβπΊ) β§ (πβ1) β (VtxβπΊ) β§ π = {β¨0, (πβ0)β©, β¨1, (πβ1)β©})) |
26 | | funcnvs2 14860 |
. . . . . . . . . . . . . . . . 17
β’ (((πβ0) β
(VtxβπΊ) β§ (πβ1) β
(VtxβπΊ) β§ (πβ0) β (πβ1)) β Fun β‘β¨β(πβ0)(πβ1)ββ©) |
27 | 26 | 3expa 1118 |
. . . . . . . . . . . . . . . 16
β’ ((((πβ0) β
(VtxβπΊ) β§ (πβ1) β
(VtxβπΊ)) β§ (πβ0) β (πβ1)) β Fun β‘β¨β(πβ0)(πβ1)ββ©) |
28 | 27 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ ((π = {β¨0, (πβ0)β©, β¨1, (πβ1)β©} β§ (((πβ0) β (VtxβπΊ) β§ (πβ1) β (VtxβπΊ)) β§ (πβ0) β (πβ1))) β Fun β‘β¨β(πβ0)(πβ1)ββ©) |
29 | | simpl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = {β¨0, (πβ0)β©, β¨1, (πβ1)β©} β§ (((πβ0) β (VtxβπΊ) β§ (πβ1) β (VtxβπΊ)) β§ (πβ0) β (πβ1))) β π = {β¨0, (πβ0)β©, β¨1, (πβ1)β©}) |
30 | | s2prop 14854 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πβ0) β
(VtxβπΊ) β§ (πβ1) β
(VtxβπΊ)) β
β¨β(πβ0)(πβ1)ββ© = {β¨0, (πβ0)β©, β¨1, (πβ1)β©}) |
31 | 30 | eqcomd 2738 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πβ0) β
(VtxβπΊ) β§ (πβ1) β
(VtxβπΊ)) β
{β¨0, (πβ0)β©, β¨1, (πβ1)β©} = β¨β(πβ0)(πβ1)ββ©) |
32 | 31 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πβ0) β
(VtxβπΊ) β§ (πβ1) β
(VtxβπΊ)) β§ (πβ0) β (πβ1)) β {β¨0,
(πβ0)β©, β¨1,
(πβ1)β©} =
β¨β(πβ0)(πβ1)ββ©) |
33 | 32 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = {β¨0, (πβ0)β©, β¨1, (πβ1)β©} β§ (((πβ0) β (VtxβπΊ) β§ (πβ1) β (VtxβπΊ)) β§ (πβ0) β (πβ1))) β {β¨0, (πβ0)β©, β¨1, (πβ1)β©} =
β¨β(πβ0)(πβ1)ββ©) |
34 | 29, 33 | eqtrd 2772 |
. . . . . . . . . . . . . . . . 17
β’ ((π = {β¨0, (πβ0)β©, β¨1, (πβ1)β©} β§ (((πβ0) β (VtxβπΊ) β§ (πβ1) β (VtxβπΊ)) β§ (πβ0) β (πβ1))) β π = β¨β(πβ0)(πβ1)ββ©) |
35 | 34 | cnveqd 5873 |
. . . . . . . . . . . . . . . 16
β’ ((π = {β¨0, (πβ0)β©, β¨1, (πβ1)β©} β§ (((πβ0) β (VtxβπΊ) β§ (πβ1) β (VtxβπΊ)) β§ (πβ0) β (πβ1))) β β‘π = β‘β¨β(πβ0)(πβ1)ββ©) |
36 | 35 | funeqd 6567 |
. . . . . . . . . . . . . . 15
β’ ((π = {β¨0, (πβ0)β©, β¨1, (πβ1)β©} β§ (((πβ0) β (VtxβπΊ) β§ (πβ1) β (VtxβπΊ)) β§ (πβ0) β (πβ1))) β (Fun β‘π β Fun β‘β¨β(πβ0)(πβ1)ββ©)) |
37 | 28, 36 | mpbird 256 |
. . . . . . . . . . . . . 14
β’ ((π = {β¨0, (πβ0)β©, β¨1, (πβ1)β©} β§ (((πβ0) β (VtxβπΊ) β§ (πβ1) β (VtxβπΊ)) β§ (πβ0) β (πβ1))) β Fun β‘π) |
38 | 37 | exp32 421 |
. . . . . . . . . . . . 13
β’ (π = {β¨0, (πβ0)β©, β¨1, (πβ1)β©} β (((πβ0) β (VtxβπΊ) β§ (πβ1) β (VtxβπΊ)) β ((πβ0) β (πβ1) β Fun β‘π))) |
39 | 38 | impcom 408 |
. . . . . . . . . . . 12
β’ ((((πβ0) β
(VtxβπΊ) β§ (πβ1) β
(VtxβπΊ)) β§ π = {β¨0, (πβ0)β©, β¨1, (πβ1)β©}) β ((πβ0) β (πβ1) β Fun β‘π)) |
40 | 39 | 3impa 1110 |
. . . . . . . . . . 11
β’ (((πβ0) β
(VtxβπΊ) β§ (πβ1) β
(VtxβπΊ) β§ π = {β¨0, (πβ0)β©, β¨1, (πβ1)β©}) β ((πβ0) β (πβ1) β Fun β‘π)) |
41 | 25, 40 | sylbi 216 |
. . . . . . . . . 10
β’ (π:{0, 1}βΆ(VtxβπΊ) β ((πβ0) β (πβ1) β Fun β‘π)) |
42 | 41 | imp 407 |
. . . . . . . . 9
β’ ((π:{0, 1}βΆ(VtxβπΊ) β§ (πβ0) β (πβ1)) β Fun β‘π) |
43 | 22, 42 | syl6bi 252 |
. . . . . . . 8
β’
(((β―βπΉ)
= 1 β§ ((πβ0) =
π΄ β§ (πβ(β―βπΉ)) = π΅)) β ((π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ π΄ β π΅) β Fun β‘π)) |
44 | 43 | expd 416 |
. . . . . . 7
β’
(((β―βπΉ)
= 1 β§ ((πβ0) =
π΄ β§ (πβ(β―βπΉ)) = π΅)) β (π:(0...(β―βπΉ))βΆ(VtxβπΊ) β (π΄ β π΅ β Fun β‘π))) |
45 | 44 | com12 32 |
. . . . . 6
β’ (π:(0...(β―βπΉ))βΆ(VtxβπΊ) β (((β―βπΉ) = 1 β§ ((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β (π΄ β π΅ β Fun β‘π))) |
46 | 45 | expd 416 |
. . . . 5
β’ (π:(0...(β―βπΉ))βΆ(VtxβπΊ) β ((β―βπΉ) = 1 β (((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β (π΄ β π΅ β Fun β‘π)))) |
47 | 46 | com34 91 |
. . . 4
β’ (π:(0...(β―βπΉ))βΆ(VtxβπΊ) β ((β―βπΉ) = 1 β (π΄ β π΅ β (((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β Fun β‘π)))) |
48 | 47 | impd 411 |
. . 3
β’ (π:(0...(β―βπΉ))βΆ(VtxβπΊ) β (((β―βπΉ) = 1 β§ π΄ β π΅) β (((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β Fun β‘π))) |
49 | 2, 48 | syl 17 |
. 2
β’ (πΉ(WalksβπΊ)π β (((β―βπΉ) = 1 β§ π΄ β π΅) β (((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β Fun β‘π))) |
50 | 49 | 3imp 1111 |
1
β’ ((πΉ(WalksβπΊ)π β§ ((β―βπΉ) = 1 β§ π΄ β π΅) β§ ((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β Fun β‘π) |