Step | Hyp | Ref
| Expression |
1 | | usgr2pthspth 26658 |
. . . . . . 7
USGraph
Paths SPaths |
2 | | usgrupgr 26077 |
. . . . . . . . 9
USGraph UPGraph |
3 | 2 | adantr 481 |
. . . . . . . 8
USGraph
UPGraph |
4 | | isspth 26620 |
. . . . . . . . . . 11
SPaths Trails |
5 | 4 | a1i 11 |
. . . . . . . . . 10
UPGraph SPaths
Trails |
6 | | usgr2pthlem.v |
. . . . . . . . . . . . 13
Vtx |
7 | | usgr2pthlem.i |
. . . . . . . . . . . . 13
iEdg |
8 | 6, 7 | upgrf1istrl 26600 |
. . . . . . . . . . . 12
UPGraph Trails
..^ ..^ |
9 | 8 | anbi1d 741 |
. . . . . . . . . . 11
UPGraph Trails ..^ ..^ |
10 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
11 | | f1eq2 6097 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ ..^ ..^ |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
13 | 12 | biimpd 219 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
14 | 13 | adantl 482 |
. . . . . . . . . . . . . . . 16
USGraph
..^ ..^ |
15 | 14 | com12 32 |
. . . . . . . . . . . . . . 15
..^ USGraph ..^ |
16 | 15 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
..^ ..^ USGraph ..^ |
17 | 16 | ad2antrl 764 |
. . . . . . . . . . . . 13
UPGraph
..^ ..^ USGraph ..^ |
18 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
|
19 | 18 | feq2d 6031 |
. . . . . . . . . . . . . . . . . . 19
|
20 | | df-f1 5893 |
. . . . . . . . . . . . . . . . . . . . 21
|
21 | 20 | simplbi2 655 |
. . . . . . . . . . . . . . . . . . . 20
|
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
23 | 19, 22 | sylbid 230 |
. . . . . . . . . . . . . . . . . 18
|
24 | 23 | adantl 482 |
. . . . . . . . . . . . . . . . 17
USGraph
|
25 | 24 | com3l 89 |
. . . . . . . . . . . . . . . 16
USGraph |
26 | 25 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . 15
..^ ..^
USGraph
|
27 | 26 | imp 445 |
. . . . . . . . . . . . . 14
..^ ..^ USGraph |
28 | 27 | adantl 482 |
. . . . . . . . . . . . 13
UPGraph
..^ ..^ USGraph |
29 | 6, 7 | usgr2pthlem 26659 |
. . . . . . . . . . . . . 14
..^ ..^ USGraph
|
30 | 29 | ad2antrl 764 |
. . . . . . . . . . . . 13
UPGraph
..^ ..^ USGraph
|
31 | 17, 28, 30 | 3jcad 1243 |
. . . . . . . . . . . 12
UPGraph
..^ ..^ USGraph ..^
|
32 | 31 | ex 450 |
. . . . . . . . . . 11
UPGraph ..^ ..^ USGraph ..^
|
33 | 9, 32 | sylbid 230 |
. . . . . . . . . 10
UPGraph Trails
USGraph
..^
|
34 | 5, 33 | sylbid 230 |
. . . . . . . . 9
UPGraph SPaths USGraph ..^
|
35 | 34 | com23 86 |
. . . . . . . 8
UPGraph USGraph SPaths ..^
|
36 | 3, 35 | mpcom 38 |
. . . . . . 7
USGraph
SPaths ..^
|
37 | 1, 36 | sylbid 230 |
. . . . . 6
USGraph
Paths ..^
|
38 | 37 | ex 450 |
. . . . 5
USGraph Paths ..^
|
39 | 38 | com13 88 |
. . . 4
Paths USGraph ..^
|
40 | 39 | imp 445 |
. . 3
Paths
USGraph ..^
|
41 | 40 | com12 32 |
. 2
USGraph Paths ..^
|
42 | | 2nn0 11309 |
. . . . . 6
|
43 | | f1f 6101 |
. . . . . 6
..^ ..^
|
44 | | fnfzo0hash 13234 |
. . . . . 6
..^
|
45 | 42, 43, 44 | sylancr 695 |
. . . . 5
..^ |
46 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
47 | 46 | eqcoms 2630 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
48 | | f1eq2 6097 |
. . . . . . . . . . . . . . . . 17
..^ ..^ ..^ ..^ |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . 16
..^
..^ |
50 | 49 | biimpd 219 |
. . . . . . . . . . . . . . 15
..^ ..^ |
51 | 50 | imp 445 |
. . . . . . . . . . . . . 14
..^
..^ |
52 | 51 | adantr 481 |
. . . . . . . . . . . . 13
..^
..^ |
53 | 52 | ad2antrr 762 |
. . . . . . . . . . . 12
..^ USGraph ..^ |
54 | | f1f 6101 |
. . . . . . . . . . . . . . 15
|
55 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . 18
|
56 | 55 | eqcoms 2630 |
. . . . . . . . . . . . . . . . 17
|
57 | 56 | adantr 481 |
. . . . . . . . . . . . . . . 16
..^
|
58 | 57 | feq2d 6031 |
. . . . . . . . . . . . . . 15
..^
|
59 | 54, 58 | syl5ib 234 |
. . . . . . . . . . . . . 14
..^
|
60 | 59 | imp 445 |
. . . . . . . . . . . . 13
..^
|
61 | 60 | ad2antrr 762 |
. . . . . . . . . . . 12
..^ USGraph |
62 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
63 | 62 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
64 | 63 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
65 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
66 | 65 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
67 | 66 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
68 | 64, 67 | preq12d 4276 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
69 | 68 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
70 | 69 | biimpcd 239 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
71 | 70 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
72 | 71 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . 21
|
73 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
74 | 73 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
75 | 74 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
76 | 67, 75 | preq12d 4276 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
77 | 76 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
78 | 77 | biimpcd 239 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
79 | 78 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
80 | 79 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . 21
|
81 | 72, 80 | jca 554 |
. . . . . . . . . . . . . . . . . . . 20
|
82 | 81 | rexlimivw 3029 |
. . . . . . . . . . . . . . . . . . 19
|
83 | 82 | rexlimivw 3029 |
. . . . . . . . . . . . . . . . . 18
|
84 | 83 | rexlimivw 3029 |
. . . . . . . . . . . . . . . . 17
|
85 | 84 | a1i13 27 |
. . . . . . . . . . . . . . . 16
USGraph |
86 | | fzo0to2pr 12553 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
87 | 10, 86 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
..^ |
88 | 87 | raleqdv 3144 |
. . . . . . . . . . . . . . . . . 18
..^ |
89 | | 2wlklem 26563 |
. . . . . . . . . . . . . . . . . 18
|
90 | 88, 89 | syl6bb 276 |
. . . . . . . . . . . . . . . . 17
..^ |
91 | 90 | imbi2d 330 |
. . . . . . . . . . . . . . . 16
USGraph ..^
USGraph |
92 | 85, 91 | sylibrd 249 |
. . . . . . . . . . . . . . 15
USGraph ..^ |
93 | 92 | ad2antrr 762 |
. . . . . . . . . . . . . 14
..^
USGraph ..^ |
94 | 93 | imp 445 |
. . . . . . . . . . . . 13
..^
USGraph ..^ |
95 | 94 | imp 445 |
. . . . . . . . . . . 12
..^ USGraph ..^ |
96 | 53, 61, 95 | 3jca 1242 |
. . . . . . . . . . 11
..^ USGraph ..^ ..^ |
97 | 20 | simprbi 480 |
. . . . . . . . . . . . 13
|
98 | 97 | adantl 482 |
. . . . . . . . . . . 12
..^
|
99 | 98 | ad2antrr 762 |
. . . . . . . . . . 11
..^ USGraph
|
100 | 96, 99 | jca 554 |
. . . . . . . . . 10
..^ USGraph ..^ ..^ |
101 | 5, 9 | bitrd 268 |
. . . . . . . . . . . 12
UPGraph SPaths
..^ ..^ |
102 | 2, 101 | syl 17 |
. . . . . . . . . . 11
USGraph SPaths
..^ ..^ |
103 | 102 | adantl 482 |
. . . . . . . . . 10
..^ USGraph SPaths
..^ ..^ |
104 | 100, 103 | mpbird 247 |
. . . . . . . . 9
..^ USGraph SPaths |
105 | | simpr 477 |
. . . . . . . . . 10
..^ USGraph USGraph |
106 | | simp-4l 806 |
. . . . . . . . . 10
..^ USGraph |
107 | 105, 106,
1 | syl2anc 693 |
. . . . . . . . 9
..^ USGraph Paths
SPaths |
108 | 104, 107 | mpbird 247 |
. . . . . . . 8
..^ USGraph Paths |
109 | 108, 106 | jca 554 |
. . . . . . 7
..^ USGraph Paths |
110 | 109 | ex 450 |
. . . . . 6
..^
USGraph Paths |
111 | 110 | exp41 638 |
. . . . 5
..^ USGraph Paths |
112 | 45, 111 | mpcom 38 |
. . . 4
..^ USGraph Paths |
113 | 112 | 3imp 1256 |
. . 3
..^
USGraph Paths |
114 | 113 | com12 32 |
. 2
USGraph ..^
Paths |
115 | 41, 114 | impbid 202 |
1
USGraph Paths ..^
|