Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’ (π β (WalksβπΊ) β¦ (2nd
βπ)) = (π β (WalksβπΊ) β¦ (2nd
βπ)) |
2 | 1 | wlkswwlksf1o 29133 |
. . . 4
β’ (πΊ β USPGraph β (π β (WalksβπΊ) β¦ (2nd
βπ)):(WalksβπΊ)β1-1-ontoβ(WWalksβπΊ)) |
3 | 2 | adantr 482 |
. . 3
β’ ((πΊ β USPGraph β§ π β β0)
β (π β
(WalksβπΊ) β¦
(2nd βπ)):(WalksβπΊ)β1-1-ontoβ(WWalksβπΊ)) |
4 | | fveqeq2 6901 |
. . . . 5
β’ (π = (2nd βπ) β ((β―βπ) = (π + 1) β (β―β(2nd
βπ)) = (π + 1))) |
5 | 4 | 3ad2ant3 1136 |
. . . 4
β’ (((πΊ β USPGraph β§ π β β0)
β§ π β
(WalksβπΊ) β§ π = (2nd βπ)) β ((β―βπ) = (π + 1) β (β―β(2nd
βπ)) = (π + 1))) |
6 | | wlkcpr 28886 |
. . . . . . 7
β’ (π β (WalksβπΊ) β (1st
βπ)(WalksβπΊ)(2nd βπ)) |
7 | | wlklenvp1 28875 |
. . . . . . . 8
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β (β―β(2nd
βπ)) =
((β―β(1st βπ)) + 1)) |
8 | | eqeq1 2737 |
. . . . . . . . . 10
β’
((β―β(2nd βπ)) = ((β―β(1st
βπ)) + 1) β
((β―β(2nd βπ)) = (π + 1) β ((β―β(1st
βπ)) + 1) = (π + 1))) |
9 | | wlkcl 28872 |
. . . . . . . . . . . . 13
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β (β―β(1st
βπ)) β
β0) |
10 | 9 | nn0cnd 12534 |
. . . . . . . . . . . 12
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β (β―β(1st
βπ)) β
β) |
11 | 10 | adantr 482 |
. . . . . . . . . . 11
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ (πΊ β USPGraph β§ π β β0)) β
(β―β(1st βπ)) β β) |
12 | | nn0cn 12482 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β) |
13 | 12 | adantl 483 |
. . . . . . . . . . . 12
β’ ((πΊ β USPGraph β§ π β β0)
β π β
β) |
14 | 13 | adantl 483 |
. . . . . . . . . . 11
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ (πΊ β USPGraph β§ π β β0)) β π β
β) |
15 | | 1cnd 11209 |
. . . . . . . . . . 11
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ (πΊ β USPGraph β§ π β β0)) β 1
β β) |
16 | 11, 14, 15 | addcan2d 11418 |
. . . . . . . . . 10
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ (πΊ β USPGraph β§ π β β0)) β
(((β―β(1st βπ)) + 1) = (π + 1) β (β―β(1st
βπ)) = π)) |
17 | 8, 16 | sylan9bbr 512 |
. . . . . . . . 9
β’
((((1st βπ)(WalksβπΊ)(2nd βπ) β§ (πΊ β USPGraph β§ π β β0)) β§
(β―β(2nd βπ)) = ((β―β(1st
βπ)) + 1)) β
((β―β(2nd βπ)) = (π + 1) β (β―β(1st
βπ)) = π)) |
18 | 17 | exp31 421 |
. . . . . . . 8
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β ((πΊ β USPGraph β§ π β β0) β
((β―β(2nd βπ)) = ((β―β(1st
βπ)) + 1) β
((β―β(2nd βπ)) = (π + 1) β (β―β(1st
βπ)) = π)))) |
19 | 7, 18 | mpid 44 |
. . . . . . 7
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β ((πΊ β USPGraph β§ π β β0) β
((β―β(2nd βπ)) = (π + 1) β (β―β(1st
βπ)) = π))) |
20 | 6, 19 | sylbi 216 |
. . . . . 6
β’ (π β (WalksβπΊ) β ((πΊ β USPGraph β§ π β β0) β
((β―β(2nd βπ)) = (π + 1) β (β―β(1st
βπ)) = π))) |
21 | 20 | impcom 409 |
. . . . 5
β’ (((πΊ β USPGraph β§ π β β0)
β§ π β
(WalksβπΊ)) β
((β―β(2nd βπ)) = (π + 1) β (β―β(1st
βπ)) = π)) |
22 | 21 | 3adant3 1133 |
. . . 4
β’ (((πΊ β USPGraph β§ π β β0)
β§ π β
(WalksβπΊ) β§ π = (2nd βπ)) β
((β―β(2nd βπ)) = (π + 1) β (β―β(1st
βπ)) = π)) |
23 | 5, 22 | bitrd 279 |
. . 3
β’ (((πΊ β USPGraph β§ π β β0)
β§ π β
(WalksβπΊ) β§ π = (2nd βπ)) β ((β―βπ) = (π + 1) β (β―β(1st
βπ)) = π)) |
24 | 1, 3, 23 | f1oresrab 7125 |
. 2
β’ ((πΊ β USPGraph β§ π β β0)
β ((π β
(WalksβπΊ) β¦
(2nd βπ))
βΎ {π β
(WalksβπΊ) β£
(β―β(1st βπ)) = π}):{π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π}β1-1-ontoβ{π β (WWalksβπΊ) β£ (β―βπ) = (π + 1)}) |
25 | | wlknwwlksnbij.f |
. . . 4
β’ πΉ = (π‘ β π β¦ (2nd βπ‘)) |
26 | | wlknwwlksnbij.t |
. . . . . . 7
β’ π = {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} |
27 | 26 | mpteq1i 5245 |
. . . . . 6
β’ (π‘ β π β¦ (2nd βπ‘)) = (π‘ β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β¦ (2nd
βπ‘)) |
28 | | ssrab2 4078 |
. . . . . . 7
β’ {π β (WalksβπΊ) β£
(β―β(1st βπ)) = π} β (WalksβπΊ) |
29 | | resmpt 6038 |
. . . . . . 7
β’ ({π β (WalksβπΊ) β£
(β―β(1st βπ)) = π} β (WalksβπΊ) β ((π‘ β (WalksβπΊ) β¦ (2nd βπ‘)) βΎ {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π}) = (π‘ β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β¦ (2nd
βπ‘))) |
30 | 28, 29 | ax-mp 5 |
. . . . . 6
β’ ((π‘ β (WalksβπΊ) β¦ (2nd
βπ‘)) βΎ {π β (WalksβπΊ) β£
(β―β(1st βπ)) = π}) = (π‘ β {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π} β¦ (2nd
βπ‘)) |
31 | | fveq2 6892 |
. . . . . . . 8
β’ (π‘ = π β (2nd βπ‘) = (2nd βπ)) |
32 | 31 | cbvmptv 5262 |
. . . . . . 7
β’ (π‘ β (WalksβπΊ) β¦ (2nd
βπ‘)) = (π β (WalksβπΊ) β¦ (2nd
βπ)) |
33 | 32 | reseq1i 5978 |
. . . . . 6
β’ ((π‘ β (WalksβπΊ) β¦ (2nd
βπ‘)) βΎ {π β (WalksβπΊ) β£
(β―β(1st βπ)) = π}) = ((π β (WalksβπΊ) β¦ (2nd βπ)) βΎ {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π}) |
34 | 27, 30, 33 | 3eqtr2i 2767 |
. . . . 5
β’ (π‘ β π β¦ (2nd βπ‘)) = ((π β (WalksβπΊ) β¦ (2nd βπ)) βΎ {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π}) |
35 | 34 | a1i 11 |
. . . 4
β’ ((πΊ β USPGraph β§ π β β0)
β (π‘ β π β¦ (2nd
βπ‘)) = ((π β (WalksβπΊ) β¦ (2nd
βπ)) βΎ {π β (WalksβπΊ) β£
(β―β(1st βπ)) = π})) |
36 | 25, 35 | eqtrid 2785 |
. . 3
β’ ((πΊ β USPGraph β§ π β β0)
β πΉ = ((π β (WalksβπΊ) β¦ (2nd
βπ)) βΎ {π β (WalksβπΊ) β£
(β―β(1st βπ)) = π})) |
37 | 26 | a1i 11 |
. . 3
β’ ((πΊ β USPGraph β§ π β β0)
β π = {π β (WalksβπΊ) β£
(β―β(1st βπ)) = π}) |
38 | | wlknwwlksnbij.w |
. . . 4
β’ π = (π WWalksN πΊ) |
39 | | wwlksn 29091 |
. . . . 5
β’ (π β β0
β (π WWalksN πΊ) = {π β (WWalksβπΊ) β£ (β―βπ) = (π + 1)}) |
40 | 39 | adantl 483 |
. . . 4
β’ ((πΊ β USPGraph β§ π β β0)
β (π WWalksN πΊ) = {π β (WWalksβπΊ) β£ (β―βπ) = (π + 1)}) |
41 | 38, 40 | eqtrid 2785 |
. . 3
β’ ((πΊ β USPGraph β§ π β β0)
β π = {π β (WWalksβπΊ) β£ (β―βπ) = (π + 1)}) |
42 | 36, 37, 41 | f1oeq123d 6828 |
. 2
β’ ((πΊ β USPGraph β§ π β β0)
β (πΉ:πβ1-1-ontoβπ β ((π β (WalksβπΊ) β¦ (2nd βπ)) βΎ {π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π}):{π β (WalksβπΊ) β£ (β―β(1st
βπ)) = π}β1-1-ontoβ{π β (WWalksβπΊ) β£ (β―βπ) = (π + 1)})) |
43 | 24, 42 | mpbird 257 |
1
β’ ((πΊ β USPGraph β§ π β β0)
β πΉ:πβ1-1-ontoβπ) |