Step | Hyp | Ref
| Expression |
1 | | frgrhash2wsp.v |
. . . . . 6
Vtx |
2 | | fusgreg2wsp.m |
. . . . . 6
WSPathsN |
3 | 1, 2 | fusgreg2wsplem 27197 |
. . . . 5
WSPathsN |
4 | 3 | adantl 482 |
. . . 4
FinUSGraph
WSPathsN |
5 | | 2nn0 11309 |
. . . . . . . . 9
|
6 | 1 | wspthsnwspthsnon 26811 |
. . . . . . . . 9
FinUSGraph WSPathsN
WSPathsNOn |
7 | 5, 6 | mpan 706 |
. . . . . . . 8
FinUSGraph WSPathsN
WSPathsNOn
|
8 | 7 | adantr 481 |
. . . . . . 7
FinUSGraph WSPathsN
WSPathsNOn |
9 | | fusgrusgr 26214 |
. . . . . . . . . 10
FinUSGraph USGraph |
10 | 9 | adantr 481 |
. . . . . . . . 9
FinUSGraph USGraph |
11 | | eqid 2622 |
. . . . . . . . . 10
Edg Edg |
12 | 1, 11 | usgr2wspthon 26858 |
. . . . . . . . 9
USGraph
WSPathsNOn
Edg
Edg |
13 | 10, 12 | sylan 488 |
. . . . . . . 8
FinUSGraph
WSPathsNOn
Edg
Edg |
14 | 13 | 2rexbidva 3056 |
. . . . . . 7
FinUSGraph
WSPathsNOn
Edg Edg |
15 | 8, 14 | bitrd 268 |
. . . . . 6
FinUSGraph WSPathsN
Edg Edg |
16 | 15 | anbi1d 741 |
. . . . 5
FinUSGraph WSPathsN
Edg
Edg |
17 | | 19.41vv 1915 |
. . . . . . 7
Edg
Edg
Edg
Edg |
18 | | velsn 4193 |
. . . . . . . . . . . 12
|
19 | 18 | bicomi 214 |
. . . . . . . . . . 11
|
20 | 19 | anbi2i 730 |
. . . . . . . . . 10
Edg
Edg
Edg
Edg
|
21 | 20 | a1i 11 |
. . . . . . . . 9
FinUSGraph Edg
Edg
Edg
Edg
|
22 | | simplr 792 |
. . . . . . . . . . . 12
FinUSGraph
|
23 | | anass 681 |
. . . . . . . . . . . . . . 15
Edg
Edg
Edg
Edg |
24 | | ancom 466 |
. . . . . . . . . . . . . . 15
Edg Edg Edg Edg |
25 | | an12 838 |
. . . . . . . . . . . . . . . . 17
Edg
Edg Edg
Edg |
26 | | nesym 2850 |
. . . . . . . . . . . . . . . . . . 19
|
27 | | prcom 4267 |
. . . . . . . . . . . . . . . . . . . 20
|
28 | 27 | eleq1i 2692 |
. . . . . . . . . . . . . . . . . . 19
Edg
Edg |
29 | 26, 28 | anbi12ci 734 |
. . . . . . . . . . . . . . . . . 18
Edg
Edg |
30 | 29 | anbi2i 730 |
. . . . . . . . . . . . . . . . 17
Edg
Edg Edg
Edg
|
31 | 25, 30 | bitri 264 |
. . . . . . . . . . . . . . . 16
Edg
Edg Edg
Edg
|
32 | 31 | anbi1i 731 |
. . . . . . . . . . . . . . 15
Edg Edg
Edg
Edg
|
33 | 23, 24, 32 | 3bitri 286 |
. . . . . . . . . . . . . 14
Edg
Edg Edg Edg
|
34 | | preq2 4269 |
. . . . . . . . . . . . . . . . 17
|
35 | 34 | eleq1d 2686 |
. . . . . . . . . . . . . . . 16
Edg
Edg |
36 | | preq2 4269 |
. . . . . . . . . . . . . . . . . 18
|
37 | 36 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
Edg
Edg |
38 | 37 | anbi1d 741 |
. . . . . . . . . . . . . . . 16
Edg
Edg
|
39 | 35, 38 | anbi12d 747 |
. . . . . . . . . . . . . . 15
Edg
Edg
Edg Edg
|
40 | | s3eq2 13615 |
. . . . . . . . . . . . . . . 16
|
41 | 40 | eqeq2d 2632 |
. . . . . . . . . . . . . . 15
|
42 | 39, 41 | anbi12d 747 |
. . . . . . . . . . . . . 14
Edg
Edg
Edg
Edg
|
43 | 33, 42 | syl5bb 272 |
. . . . . . . . . . . . 13
Edg
Edg Edg Edg
|
44 | 43 | adantl 482 |
. . . . . . . . . . . 12
FinUSGraph
Edg
Edg Edg Edg
|
45 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . 20
|
46 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . 21
|
47 | | s3fv1 13637 |
. . . . . . . . . . . . . . . . . . . . 21
|
48 | 46, 47 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
|
49 | 45, 48 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
|
50 | 49 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . 18
|
51 | 50 | biimpd 219 |
. . . . . . . . . . . . . . . . 17
|
52 | 51 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
53 | 52 | adantr 481 |
. . . . . . . . . . . . . . 15
Edg
Edg
|
54 | 53 | com12 32 |
. . . . . . . . . . . . . 14
Edg
Edg
|
55 | 54 | ad2antll 765 |
. . . . . . . . . . . . 13
FinUSGraph
Edg
Edg
|
56 | 55 | imp 445 |
. . . . . . . . . . . 12
FinUSGraph
Edg
Edg |
57 | 22, 44, 56 | rspcebdv 3314 |
. . . . . . . . . . 11
FinUSGraph
Edg
Edg Edg Edg
|
58 | 57 | pm5.32da 673 |
. . . . . . . . . 10
FinUSGraph
Edg
Edg
Edg
Edg
|
59 | | an32 839 |
. . . . . . . . . . 11
Edg
Edg
Edg
Edg |
60 | 59 | a1i 11 |
. . . . . . . . . 10
FinUSGraph
Edg
Edg
Edg
Edg |
61 | | usgrumgr 26074 |
. . . . . . . . . . . . . . . . . 18
USGraph UMGraph |
62 | 1, 11 | umgrpredgv 26035 |
. . . . . . . . . . . . . . . . . . . . 21
UMGraph
Edg |
63 | 62 | simpld 475 |
. . . . . . . . . . . . . . . . . . . 20
UMGraph
Edg |
64 | 63 | ex 450 |
. . . . . . . . . . . . . . . . . . 19
UMGraph Edg
|
65 | 1, 11 | umgrpredgv 26035 |
. . . . . . . . . . . . . . . . . . . . . . 23
UMGraph
Edg |
66 | 65 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . 22
UMGraph
Edg |
67 | 66 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . 21
Edg UMGraph |
68 | 67 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
Edg
UMGraph |
69 | 68 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
UMGraph Edg
|
70 | 64, 69 | anim12d 586 |
. . . . . . . . . . . . . . . . . 18
UMGraph Edg Edg
|
71 | 9, 61, 70 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
FinUSGraph Edg Edg
|
72 | 71 | adantr 481 |
. . . . . . . . . . . . . . . 16
FinUSGraph Edg
Edg
|
73 | 72 | com12 32 |
. . . . . . . . . . . . . . 15
Edg
Edg FinUSGraph
|
74 | 73 | adantr 481 |
. . . . . . . . . . . . . 14
Edg
Edg
FinUSGraph
|
75 | 74 | impcom 446 |
. . . . . . . . . . . . 13
FinUSGraph Edg
Edg
|
76 | | fveq1 6190 |
. . . . . . . . . . . . . . 15
|
77 | 76 | adantl 482 |
. . . . . . . . . . . . . 14
Edg
Edg
|
78 | | s3fv1 13637 |
. . . . . . . . . . . . . . 15
|
79 | 78 | adantl 482 |
. . . . . . . . . . . . . 14
FinUSGraph |
80 | 77, 79 | sylan9eqr 2678 |
. . . . . . . . . . . . 13
FinUSGraph Edg
Edg
|
81 | 75, 80 | jca 554 |
. . . . . . . . . . . 12
FinUSGraph Edg
Edg
|
82 | 81 | ex 450 |
. . . . . . . . . . 11
FinUSGraph Edg
Edg
|
83 | 82 | pm4.71rd 667 |
. . . . . . . . . 10
FinUSGraph Edg
Edg
Edg
Edg
|
84 | 58, 60, 83 | 3bitr4d 300 |
. . . . . . . . 9
FinUSGraph
Edg
Edg
Edg
Edg |
85 | 11 | nbusgreledg 26249 |
. . . . . . . . . . . . 13
USGraph NeighbVtx
Edg |
86 | 9, 85 | syl 17 |
. . . . . . . . . . . 12
FinUSGraph NeighbVtx
Edg |
87 | 86 | adantr 481 |
. . . . . . . . . . 11
FinUSGraph NeighbVtx
Edg |
88 | | eldif 3584 |
. . . . . . . . . . . 12
NeighbVtx
NeighbVtx
|
89 | 11 | nbusgreledg 26249 |
. . . . . . . . . . . . . . 15
USGraph NeighbVtx
Edg |
90 | 9, 89 | syl 17 |
. . . . . . . . . . . . . 14
FinUSGraph NeighbVtx
Edg |
91 | 90 | adantr 481 |
. . . . . . . . . . . . 13
FinUSGraph NeighbVtx
Edg |
92 | | velsn 4193 |
. . . . . . . . . . . . . . 15
|
93 | 92 | a1i 11 |
. . . . . . . . . . . . . 14
FinUSGraph |
94 | 93 | notbid 308 |
. . . . . . . . . . . . 13
FinUSGraph
|
95 | 91, 94 | anbi12d 747 |
. . . . . . . . . . . 12
FinUSGraph NeighbVtx
Edg |
96 | 88, 95 | syl5bb 272 |
. . . . . . . . . . 11
FinUSGraph NeighbVtx
Edg |
97 | 87, 96 | anbi12d 747 |
. . . . . . . . . 10
FinUSGraph NeighbVtx NeighbVtx
Edg Edg
|
98 | 97 | anbi1d 741 |
. . . . . . . . 9
FinUSGraph NeighbVtx
NeighbVtx Edg
Edg
|
99 | 21, 84, 98 | 3bitr4d 300 |
. . . . . . . 8
FinUSGraph
Edg
Edg
NeighbVtx NeighbVtx |
100 | 99 | 2exbidv 1852 |
. . . . . . 7
FinUSGraph
Edg
Edg
NeighbVtx NeighbVtx
|
101 | 17, 100 | syl5bbr 274 |
. . . . . 6
FinUSGraph
Edg
Edg
NeighbVtx NeighbVtx
|
102 | | r2ex 3061 |
. . . . . . 7
Edg
Edg
Edg
Edg |
103 | 102 | anbi1i 731 |
. . . . . 6
Edg
Edg
Edg
Edg |
104 | | r2ex 3061 |
. . . . . 6
NeighbVtx NeighbVtx
NeighbVtx NeighbVtx
|
105 | 101, 103,
104 | 3bitr4g 303 |
. . . . 5
FinUSGraph
Edg
Edg
NeighbVtx
NeighbVtx |
106 | | vex 3203 |
. . . . . . . 8
|
107 | | eleq1w 2684 |
. . . . . . . . 9
|
108 | 107 | 2rexbidv 3057 |
. . . . . . . 8
NeighbVtx NeighbVtx
NeighbVtx
NeighbVtx |
109 | 106, 108 | elab 3350 |
. . . . . . 7
NeighbVtx NeighbVtx NeighbVtx NeighbVtx |
110 | 109 | bicomi 214 |
. . . . . 6
NeighbVtx NeighbVtx
NeighbVtx
NeighbVtx |
111 | 110 | a1i 11 |
. . . . 5
FinUSGraph
NeighbVtx NeighbVtx
NeighbVtx
NeighbVtx |
112 | 16, 105, 111 | 3bitrd 294 |
. . . 4
FinUSGraph WSPathsN
NeighbVtx
NeighbVtx |
113 | 4, 112 | bitrd 268 |
. . 3
FinUSGraph
NeighbVtx
NeighbVtx |
114 | 113 | eqrdv 2620 |
. 2
FinUSGraph
NeighbVtx NeighbVtx |
115 | | dfiunv2 4556 |
. 2
NeighbVtx
NeighbVtx NeighbVtx NeighbVtx |
116 | 114, 115 | syl6eqr 2674 |
1
FinUSGraph NeighbVtx NeighbVtx |