Step | Hyp | Ref
| Expression |
1 | | fvex 6902 |
. . . . . 6
โข
(1st โ๐ค) โ V |
2 | | breq1 5151 |
. . . . . 6
โข (๐ = (1st โ๐ค) โ (๐(Walksโ๐บ)(2nd โ๐ค) โ (1st โ๐ค)(Walksโ๐บ)(2nd โ๐ค))) |
3 | 1, 2 | spcev 3597 |
. . . . 5
โข
((1st โ๐ค)(Walksโ๐บ)(2nd โ๐ค) โ โ๐ ๐(Walksโ๐บ)(2nd โ๐ค)) |
4 | | wlkiswwlks 29120 |
. . . . 5
โข (๐บ โ USPGraph โ
(โ๐ ๐(Walksโ๐บ)(2nd โ๐ค) โ (2nd โ๐ค) โ (WWalksโ๐บ))) |
5 | 3, 4 | imbitrid 243 |
. . . 4
โข (๐บ โ USPGraph โ
((1st โ๐ค)(Walksโ๐บ)(2nd โ๐ค) โ (2nd โ๐ค) โ (WWalksโ๐บ))) |
6 | | wlkcpr 28876 |
. . . . 5
โข (๐ค โ (Walksโ๐บ) โ (1st
โ๐ค)(Walksโ๐บ)(2nd โ๐ค)) |
7 | 6 | biimpi 215 |
. . . 4
โข (๐ค โ (Walksโ๐บ) โ (1st
โ๐ค)(Walksโ๐บ)(2nd โ๐ค)) |
8 | 5, 7 | impel 507 |
. . 3
โข ((๐บ โ USPGraph โง ๐ค โ (Walksโ๐บ)) โ (2nd
โ๐ค) โ
(WWalksโ๐บ)) |
9 | | wlkswwlksf1o.f |
. . 3
โข ๐น = (๐ค โ (Walksโ๐บ) โฆ (2nd โ๐ค)) |
10 | 8, 9 | fmptd 7111 |
. 2
โข (๐บ โ USPGraph โ ๐น:(Walksโ๐บ)โถ(WWalksโ๐บ)) |
11 | | simpr 486 |
. . . 4
โข ((๐บ โ USPGraph โง ๐น:(Walksโ๐บ)โถ(WWalksโ๐บ)) โ ๐น:(Walksโ๐บ)โถ(WWalksโ๐บ)) |
12 | | fveq2 6889 |
. . . . . . . . 9
โข (๐ค = ๐ฅ โ (2nd โ๐ค) = (2nd โ๐ฅ)) |
13 | | id 22 |
. . . . . . . . 9
โข (๐ฅ โ (Walksโ๐บ) โ ๐ฅ โ (Walksโ๐บ)) |
14 | | fvexd 6904 |
. . . . . . . . 9
โข (๐ฅ โ (Walksโ๐บ) โ (2nd
โ๐ฅ) โ
V) |
15 | 9, 12, 13, 14 | fvmptd3 7019 |
. . . . . . . 8
โข (๐ฅ โ (Walksโ๐บ) โ (๐นโ๐ฅ) = (2nd โ๐ฅ)) |
16 | | fveq2 6889 |
. . . . . . . . 9
โข (๐ค = ๐ฆ โ (2nd โ๐ค) = (2nd โ๐ฆ)) |
17 | | id 22 |
. . . . . . . . 9
โข (๐ฆ โ (Walksโ๐บ) โ ๐ฆ โ (Walksโ๐บ)) |
18 | | fvexd 6904 |
. . . . . . . . 9
โข (๐ฆ โ (Walksโ๐บ) โ (2nd
โ๐ฆ) โ
V) |
19 | 9, 16, 17, 18 | fvmptd3 7019 |
. . . . . . . 8
โข (๐ฆ โ (Walksโ๐บ) โ (๐นโ๐ฆ) = (2nd โ๐ฆ)) |
20 | 15, 19 | eqeqan12d 2747 |
. . . . . . 7
โข ((๐ฅ โ (Walksโ๐บ) โง ๐ฆ โ (Walksโ๐บ)) โ ((๐นโ๐ฅ) = (๐นโ๐ฆ) โ (2nd โ๐ฅ) = (2nd โ๐ฆ))) |
21 | 20 | adantl 483 |
. . . . . 6
โข (((๐บ โ USPGraph โง ๐น:(Walksโ๐บ)โถ(WWalksโ๐บ)) โง (๐ฅ โ (Walksโ๐บ) โง ๐ฆ โ (Walksโ๐บ))) โ ((๐นโ๐ฅ) = (๐นโ๐ฆ) โ (2nd โ๐ฅ) = (2nd โ๐ฆ))) |
22 | | uspgr2wlkeqi 28895 |
. . . . . . . 8
โข ((๐บ โ USPGraph โง (๐ฅ โ (Walksโ๐บ) โง ๐ฆ โ (Walksโ๐บ)) โง (2nd โ๐ฅ) = (2nd โ๐ฆ)) โ ๐ฅ = ๐ฆ) |
23 | 22 | ad4ant134 1175 |
. . . . . . 7
โข ((((๐บ โ USPGraph โง ๐น:(Walksโ๐บ)โถ(WWalksโ๐บ)) โง (๐ฅ โ (Walksโ๐บ) โง ๐ฆ โ (Walksโ๐บ))) โง (2nd โ๐ฅ) = (2nd โ๐ฆ)) โ ๐ฅ = ๐ฆ) |
24 | 23 | ex 414 |
. . . . . 6
โข (((๐บ โ USPGraph โง ๐น:(Walksโ๐บ)โถ(WWalksโ๐บ)) โง (๐ฅ โ (Walksโ๐บ) โง ๐ฆ โ (Walksโ๐บ))) โ ((2nd โ๐ฅ) = (2nd โ๐ฆ) โ ๐ฅ = ๐ฆ)) |
25 | 21, 24 | sylbid 239 |
. . . . 5
โข (((๐บ โ USPGraph โง ๐น:(Walksโ๐บ)โถ(WWalksโ๐บ)) โง (๐ฅ โ (Walksโ๐บ) โง ๐ฆ โ (Walksโ๐บ))) โ ((๐นโ๐ฅ) = (๐นโ๐ฆ) โ ๐ฅ = ๐ฆ)) |
26 | 25 | ralrimivva 3201 |
. . . 4
โข ((๐บ โ USPGraph โง ๐น:(Walksโ๐บ)โถ(WWalksโ๐บ)) โ โ๐ฅ โ (Walksโ๐บ)โ๐ฆ โ (Walksโ๐บ)((๐นโ๐ฅ) = (๐นโ๐ฆ) โ ๐ฅ = ๐ฆ)) |
27 | | dff13 7251 |
. . . 4
โข (๐น:(Walksโ๐บ)โ1-1โ(WWalksโ๐บ) โ (๐น:(Walksโ๐บ)โถ(WWalksโ๐บ) โง โ๐ฅ โ (Walksโ๐บ)โ๐ฆ โ (Walksโ๐บ)((๐นโ๐ฅ) = (๐นโ๐ฆ) โ ๐ฅ = ๐ฆ))) |
28 | 11, 26, 27 | sylanbrc 584 |
. . 3
โข ((๐บ โ USPGraph โง ๐น:(Walksโ๐บ)โถ(WWalksโ๐บ)) โ ๐น:(Walksโ๐บ)โ1-1โ(WWalksโ๐บ)) |
29 | | wlkiswwlks 29120 |
. . . . . . . . . 10
โข (๐บ โ USPGraph โ
(โ๐ ๐(Walksโ๐บ)๐ฆ โ ๐ฆ โ (WWalksโ๐บ))) |
30 | 29 | adantr 482 |
. . . . . . . . 9
โข ((๐บ โ USPGraph โง ๐น:(Walksโ๐บ)โถ(WWalksโ๐บ)) โ (โ๐ ๐(Walksโ๐บ)๐ฆ โ ๐ฆ โ (WWalksโ๐บ))) |
31 | | df-br 5149 |
. . . . . . . . . . 11
โข (๐(Walksโ๐บ)๐ฆ โ โจ๐, ๐ฆโฉ โ (Walksโ๐บ)) |
32 | | vex 3479 |
. . . . . . . . . . . . . 14
โข ๐ โ V |
33 | | vex 3479 |
. . . . . . . . . . . . . 14
โข ๐ฆ โ V |
34 | 32, 33 | op2nd 7981 |
. . . . . . . . . . . . 13
โข
(2nd โโจ๐, ๐ฆโฉ) = ๐ฆ |
35 | 34 | eqcomi 2742 |
. . . . . . . . . . . 12
โข ๐ฆ = (2nd
โโจ๐, ๐ฆโฉ) |
36 | | opex 5464 |
. . . . . . . . . . . . 13
โข
โจ๐, ๐ฆโฉ โ V |
37 | | eleq1 2822 |
. . . . . . . . . . . . . 14
โข (๐ฅ = โจ๐, ๐ฆโฉ โ (๐ฅ โ (Walksโ๐บ) โ โจ๐, ๐ฆโฉ โ (Walksโ๐บ))) |
38 | | fveq2 6889 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = โจ๐, ๐ฆโฉ โ (2nd โ๐ฅ) = (2nd
โโจ๐, ๐ฆโฉ)) |
39 | 38 | eqeq2d 2744 |
. . . . . . . . . . . . . 14
โข (๐ฅ = โจ๐, ๐ฆโฉ โ (๐ฆ = (2nd โ๐ฅ) โ ๐ฆ = (2nd โโจ๐, ๐ฆโฉ))) |
40 | 37, 39 | anbi12d 632 |
. . . . . . . . . . . . 13
โข (๐ฅ = โจ๐, ๐ฆโฉ โ ((๐ฅ โ (Walksโ๐บ) โง ๐ฆ = (2nd โ๐ฅ)) โ (โจ๐, ๐ฆโฉ โ (Walksโ๐บ) โง ๐ฆ = (2nd โโจ๐, ๐ฆโฉ)))) |
41 | 36, 40 | spcev 3597 |
. . . . . . . . . . . 12
โข
((โจ๐, ๐ฆโฉ โ (Walksโ๐บ) โง ๐ฆ = (2nd โโจ๐, ๐ฆโฉ)) โ โ๐ฅ(๐ฅ โ (Walksโ๐บ) โง ๐ฆ = (2nd โ๐ฅ))) |
42 | 35, 41 | mpan2 690 |
. . . . . . . . . . 11
โข
(โจ๐, ๐ฆโฉ โ (Walksโ๐บ) โ โ๐ฅ(๐ฅ โ (Walksโ๐บ) โง ๐ฆ = (2nd โ๐ฅ))) |
43 | 31, 42 | sylbi 216 |
. . . . . . . . . 10
โข (๐(Walksโ๐บ)๐ฆ โ โ๐ฅ(๐ฅ โ (Walksโ๐บ) โง ๐ฆ = (2nd โ๐ฅ))) |
44 | 43 | exlimiv 1934 |
. . . . . . . . 9
โข
(โ๐ ๐(Walksโ๐บ)๐ฆ โ โ๐ฅ(๐ฅ โ (Walksโ๐บ) โง ๐ฆ = (2nd โ๐ฅ))) |
45 | 30, 44 | syl6bir 254 |
. . . . . . . 8
โข ((๐บ โ USPGraph โง ๐น:(Walksโ๐บ)โถ(WWalksโ๐บ)) โ (๐ฆ โ (WWalksโ๐บ) โ โ๐ฅ(๐ฅ โ (Walksโ๐บ) โง ๐ฆ = (2nd โ๐ฅ)))) |
46 | 45 | imp 408 |
. . . . . . 7
โข (((๐บ โ USPGraph โง ๐น:(Walksโ๐บ)โถ(WWalksโ๐บ)) โง ๐ฆ โ (WWalksโ๐บ)) โ โ๐ฅ(๐ฅ โ (Walksโ๐บ) โง ๐ฆ = (2nd โ๐ฅ))) |
47 | | df-rex 3072 |
. . . . . . 7
โข
(โ๐ฅ โ
(Walksโ๐บ)๐ฆ = (2nd โ๐ฅ) โ โ๐ฅ(๐ฅ โ (Walksโ๐บ) โง ๐ฆ = (2nd โ๐ฅ))) |
48 | 46, 47 | sylibr 233 |
. . . . . 6
โข (((๐บ โ USPGraph โง ๐น:(Walksโ๐บ)โถ(WWalksโ๐บ)) โง ๐ฆ โ (WWalksโ๐บ)) โ โ๐ฅ โ (Walksโ๐บ)๐ฆ = (2nd โ๐ฅ)) |
49 | 15 | eqeq2d 2744 |
. . . . . . 7
โข (๐ฅ โ (Walksโ๐บ) โ (๐ฆ = (๐นโ๐ฅ) โ ๐ฆ = (2nd โ๐ฅ))) |
50 | 49 | rexbiia 3093 |
. . . . . 6
โข
(โ๐ฅ โ
(Walksโ๐บ)๐ฆ = (๐นโ๐ฅ) โ โ๐ฅ โ (Walksโ๐บ)๐ฆ = (2nd โ๐ฅ)) |
51 | 48, 50 | sylibr 233 |
. . . . 5
โข (((๐บ โ USPGraph โง ๐น:(Walksโ๐บ)โถ(WWalksโ๐บ)) โง ๐ฆ โ (WWalksโ๐บ)) โ โ๐ฅ โ (Walksโ๐บ)๐ฆ = (๐นโ๐ฅ)) |
52 | 51 | ralrimiva 3147 |
. . . 4
โข ((๐บ โ USPGraph โง ๐น:(Walksโ๐บ)โถ(WWalksโ๐บ)) โ โ๐ฆ โ (WWalksโ๐บ)โ๐ฅ โ (Walksโ๐บ)๐ฆ = (๐นโ๐ฅ)) |
53 | | dffo3 7101 |
. . . 4
โข (๐น:(Walksโ๐บ)โontoโ(WWalksโ๐บ) โ (๐น:(Walksโ๐บ)โถ(WWalksโ๐บ) โง โ๐ฆ โ (WWalksโ๐บ)โ๐ฅ โ (Walksโ๐บ)๐ฆ = (๐นโ๐ฅ))) |
54 | 11, 52, 53 | sylanbrc 584 |
. . 3
โข ((๐บ โ USPGraph โง ๐น:(Walksโ๐บ)โถ(WWalksโ๐บ)) โ ๐น:(Walksโ๐บ)โontoโ(WWalksโ๐บ)) |
55 | | df-f1o 6548 |
. . 3
โข (๐น:(Walksโ๐บ)โ1-1-ontoโ(WWalksโ๐บ) โ (๐น:(Walksโ๐บ)โ1-1โ(WWalksโ๐บ) โง ๐น:(Walksโ๐บ)โontoโ(WWalksโ๐บ))) |
56 | 28, 54, 55 | sylanbrc 584 |
. 2
โข ((๐บ โ USPGraph โง ๐น:(Walksโ๐บ)โถ(WWalksโ๐บ)) โ ๐น:(Walksโ๐บ)โ1-1-ontoโ(WWalksโ๐บ)) |
57 | 10, 56 | mpdan 686 |
1
โข (๐บ โ USPGraph โ ๐น:(Walksโ๐บ)โ1-1-ontoโ(WWalksโ๐บ)) |