Step | Hyp | Ref
| Expression |
1 | | conngrv2edg.v |
. . . 4
β’ π = (VtxβπΊ) |
2 | 1 | fvexi 6906 |
. . 3
β’ π β V |
3 | | simp3 1139 |
. . 3
β’ ((πΊ β ConnGraph β§ π β π β§ 1 < (β―βπ)) β 1 <
(β―βπ)) |
4 | | simp2 1138 |
. . 3
β’ ((πΊ β ConnGraph β§ π β π β§ 1 < (β―βπ)) β π β π) |
5 | | hashgt12el2 14383 |
. . 3
β’ ((π β V β§ 1 <
(β―βπ) β§
π β π) β βπ£ β π π β π£) |
6 | 2, 3, 4, 5 | mp3an2i 1467 |
. 2
β’ ((πΊ β ConnGraph β§ π β π β§ 1 < (β―βπ)) β βπ£ β π π β π£) |
7 | 1 | isconngr 29442 |
. . . . . . . 8
β’ (πΊ β ConnGraph β (πΊ β ConnGraph β
βπ β π βπ β π βπβπ π(π(PathsOnβπΊ)π)π)) |
8 | | oveq1 7416 |
. . . . . . . . . . . . 13
β’ (π = π β (π(PathsOnβπΊ)π) = (π(PathsOnβπΊ)π)) |
9 | 8 | breqd 5160 |
. . . . . . . . . . . 12
β’ (π = π β (π(π(PathsOnβπΊ)π)π β π(π(PathsOnβπΊ)π)π)) |
10 | 9 | 2exbidv 1928 |
. . . . . . . . . . 11
β’ (π = π β (βπβπ π(π(PathsOnβπΊ)π)π β βπβπ π(π(PathsOnβπΊ)π)π)) |
11 | | oveq2 7417 |
. . . . . . . . . . . . 13
β’ (π = π£ β (π(PathsOnβπΊ)π) = (π(PathsOnβπΊ)π£)) |
12 | 11 | breqd 5160 |
. . . . . . . . . . . 12
β’ (π = π£ β (π(π(PathsOnβπΊ)π)π β π(π(PathsOnβπΊ)π£)π)) |
13 | 12 | 2exbidv 1928 |
. . . . . . . . . . 11
β’ (π = π£ β (βπβπ π(π(PathsOnβπΊ)π)π β βπβπ π(π(PathsOnβπΊ)π£)π)) |
14 | 10, 13 | rspc2v 3623 |
. . . . . . . . . 10
β’ ((π β π β§ π£ β π) β (βπ β π βπ β π βπβπ π(π(PathsOnβπΊ)π)π β βπβπ π(π(PathsOnβπΊ)π£)π)) |
15 | 14 | ad2ant2r 746 |
. . . . . . . . 9
β’ (((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£)) β (βπ β π βπ β π βπβπ π(π(PathsOnβπΊ)π)π β βπβπ π(π(PathsOnβπΊ)π£)π)) |
16 | | pthontrlon 29004 |
. . . . . . . . . . . 12
β’ (π(π(PathsOnβπΊ)π£)π β π(π(TrailsOnβπΊ)π£)π) |
17 | | trlsonwlkon 28967 |
. . . . . . . . . . . 12
β’ (π(π(TrailsOnβπΊ)π£)π β π(π(WalksOnβπΊ)π£)π) |
18 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π(π(WalksOnβπΊ)π£)π β§ ((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£))) β π(π(WalksOnβπΊ)π£)π) |
19 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ (((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£)) β π β π£) |
20 | | wlkon2n0 28923 |
. . . . . . . . . . . . . . 15
β’ ((π(π(WalksOnβπΊ)π£)π β§ π β π£) β (β―βπ) β 0) |
21 | 19, 20 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((π(π(WalksOnβπΊ)π£)π β§ ((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£))) β (β―βπ) β 0) |
22 | 18, 21 | jca 513 |
. . . . . . . . . . . . 13
β’ ((π(π(WalksOnβπΊ)π£)π β§ ((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£))) β (π(π(WalksOnβπΊ)π£)π β§ (β―βπ) β 0)) |
23 | 22 | ex 414 |
. . . . . . . . . . . 12
β’ (π(π(WalksOnβπΊ)π£)π β (((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£)) β (π(π(WalksOnβπΊ)π£)π β§ (β―βπ) β 0))) |
24 | 16, 17, 23 | 3syl 18 |
. . . . . . . . . . 11
β’ (π(π(PathsOnβπΊ)π£)π β (((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£)) β (π(π(WalksOnβπΊ)π£)π β§ (β―βπ) β 0))) |
25 | | conngrv2edg.i |
. . . . . . . . . . . 12
β’ πΌ = (iEdgβπΊ) |
26 | 25 | wlkonl1iedg 28922 |
. . . . . . . . . . 11
β’ ((π(π(WalksOnβπΊ)π£)π β§ (β―βπ) β 0) β βπ β ran πΌ π β π) |
27 | 24, 26 | syl6com 37 |
. . . . . . . . . 10
β’ (((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£)) β (π(π(PathsOnβπΊ)π£)π β βπ β ran πΌ π β π)) |
28 | 27 | exlimdvv 1938 |
. . . . . . . . 9
β’ (((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£)) β (βπβπ π(π(PathsOnβπΊ)π£)π β βπ β ran πΌ π β π)) |
29 | 15, 28 | syldc 48 |
. . . . . . . 8
β’
(βπ β
π βπ β π βπβπ π(π(PathsOnβπΊ)π)π β (((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£)) β βπ β ran πΌ π β π)) |
30 | 7, 29 | syl6bi 253 |
. . . . . . 7
β’ (πΊ β ConnGraph β (πΊ β ConnGraph β
(((π β π β§ 1 <
(β―βπ)) β§
(π£ β π β§ π β π£)) β βπ β ran πΌ π β π))) |
31 | 30 | pm2.43i 52 |
. . . . . 6
β’ (πΊ β ConnGraph β
(((π β π β§ 1 <
(β―βπ)) β§
(π£ β π β§ π β π£)) β βπ β ran πΌ π β π)) |
32 | 31 | expd 417 |
. . . . 5
β’ (πΊ β ConnGraph β ((π β π β§ 1 < (β―βπ)) β ((π£ β π β§ π β π£) β βπ β ran πΌ π β π))) |
33 | 32 | 3impib 1117 |
. . . 4
β’ ((πΊ β ConnGraph β§ π β π β§ 1 < (β―βπ)) β ((π£ β π β§ π β π£) β βπ β ran πΌ π β π)) |
34 | 33 | expd 417 |
. . 3
β’ ((πΊ β ConnGraph β§ π β π β§ 1 < (β―βπ)) β (π£ β π β (π β π£ β βπ β ran πΌ π β π))) |
35 | 34 | rexlimdv 3154 |
. 2
β’ ((πΊ β ConnGraph β§ π β π β§ 1 < (β―βπ)) β (βπ£ β π π β π£ β βπ β ran πΌ π β π)) |
36 | 6, 35 | mpd 15 |
1
β’ ((πΊ β ConnGraph β§ π β π β§ 1 < (β―βπ)) β βπ β ran πΌ π β π) |