Step | Hyp | Ref
| Expression |
1 | | conngrv2edg.v |
. . . 4
β’ π = (VtxβπΊ) |
2 | 1 | fvexi 6905 |
. . 3
β’ π β V |
3 | | simp3 1138 |
. . 3
β’ ((πΊ β ConnGraph β§ π β π β§ 1 < (β―βπ)) β 1 <
(β―βπ)) |
4 | | simp2 1137 |
. . 3
β’ ((πΊ β ConnGraph β§ π β π β§ 1 < (β―βπ)) β π β π) |
5 | | hashgt12el2 14385 |
. . 3
β’ ((π β V β§ 1 <
(β―βπ) β§
π β π) β βπ£ β π π β π£) |
6 | 2, 3, 4, 5 | mp3an2i 1466 |
. 2
β’ ((πΊ β ConnGraph β§ π β π β§ 1 < (β―βπ)) β βπ£ β π π β π£) |
7 | 1 | isconngr 29480 |
. . . . . . . 8
β’ (πΊ β ConnGraph β (πΊ β ConnGraph β
βπ β π βπ β π βπβπ π(π(PathsOnβπΊ)π)π)) |
8 | | oveq1 7418 |
. . . . . . . . . . . . 13
β’ (π = π β (π(PathsOnβπΊ)π) = (π(PathsOnβπΊ)π)) |
9 | 8 | breqd 5159 |
. . . . . . . . . . . 12
β’ (π = π β (π(π(PathsOnβπΊ)π)π β π(π(PathsOnβπΊ)π)π)) |
10 | 9 | 2exbidv 1927 |
. . . . . . . . . . 11
β’ (π = π β (βπβπ π(π(PathsOnβπΊ)π)π β βπβπ π(π(PathsOnβπΊ)π)π)) |
11 | | oveq2 7419 |
. . . . . . . . . . . . 13
β’ (π = π£ β (π(PathsOnβπΊ)π) = (π(PathsOnβπΊ)π£)) |
12 | 11 | breqd 5159 |
. . . . . . . . . . . 12
β’ (π = π£ β (π(π(PathsOnβπΊ)π)π β π(π(PathsOnβπΊ)π£)π)) |
13 | 12 | 2exbidv 1927 |
. . . . . . . . . . 11
β’ (π = π£ β (βπβπ π(π(PathsOnβπΊ)π)π β βπβπ π(π(PathsOnβπΊ)π£)π)) |
14 | 10, 13 | rspc2v 3622 |
. . . . . . . . . 10
β’ ((π β π β§ π£ β π) β (βπ β π βπ β π βπβπ π(π(PathsOnβπΊ)π)π β βπβπ π(π(PathsOnβπΊ)π£)π)) |
15 | 14 | ad2ant2r 745 |
. . . . . . . . 9
β’ (((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£)) β (βπ β π βπ β π βπβπ π(π(PathsOnβπΊ)π)π β βπβπ π(π(PathsOnβπΊ)π£)π)) |
16 | | pthontrlon 29042 |
. . . . . . . . . . . 12
β’ (π(π(PathsOnβπΊ)π£)π β π(π(TrailsOnβπΊ)π£)π) |
17 | | trlsonwlkon 29005 |
. . . . . . . . . . . 12
β’ (π(π(TrailsOnβπΊ)π£)π β π(π(WalksOnβπΊ)π£)π) |
18 | | simpl 483 |
. . . . . . . . . . . . . 14
β’ ((π(π(WalksOnβπΊ)π£)π β§ ((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£))) β π(π(WalksOnβπΊ)π£)π) |
19 | | simprr 771 |
. . . . . . . . . . . . . . 15
β’ (((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£)) β π β π£) |
20 | | wlkon2n0 28961 |
. . . . . . . . . . . . . . 15
β’ ((π(π(WalksOnβπΊ)π£)π β§ π β π£) β (β―βπ) β 0) |
21 | 19, 20 | sylan2 593 |
. . . . . . . . . . . . . 14
β’ ((π(π(WalksOnβπΊ)π£)π β§ ((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£))) β (β―βπ) β 0) |
22 | 18, 21 | jca 512 |
. . . . . . . . . . . . 13
β’ ((π(π(WalksOnβπΊ)π£)π β§ ((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£))) β (π(π(WalksOnβπΊ)π£)π β§ (β―βπ) β 0)) |
23 | 22 | ex 413 |
. . . . . . . . . . . 12
β’ (π(π(WalksOnβπΊ)π£)π β (((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£)) β (π(π(WalksOnβπΊ)π£)π β§ (β―βπ) β 0))) |
24 | 16, 17, 23 | 3syl 18 |
. . . . . . . . . . 11
β’ (π(π(PathsOnβπΊ)π£)π β (((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£)) β (π(π(WalksOnβπΊ)π£)π β§ (β―βπ) β 0))) |
25 | | conngrv2edg.i |
. . . . . . . . . . . 12
β’ πΌ = (iEdgβπΊ) |
26 | 25 | wlkonl1iedg 28960 |
. . . . . . . . . . 11
β’ ((π(π(WalksOnβπΊ)π£)π β§ (β―βπ) β 0) β βπ β ran πΌ π β π) |
27 | 24, 26 | syl6com 37 |
. . . . . . . . . 10
β’ (((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£)) β (π(π(PathsOnβπΊ)π£)π β βπ β ran πΌ π β π)) |
28 | 27 | exlimdvv 1937 |
. . . . . . . . 9
β’ (((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£)) β (βπβπ π(π(PathsOnβπΊ)π£)π β βπ β ran πΌ π β π)) |
29 | 15, 28 | syldc 48 |
. . . . . . . 8
β’
(βπ β
π βπ β π βπβπ π(π(PathsOnβπΊ)π)π β (((π β π β§ 1 < (β―βπ)) β§ (π£ β π β§ π β π£)) β βπ β ran πΌ π β π)) |
30 | 7, 29 | syl6bi 252 |
. . . . . . 7
β’ (πΊ β ConnGraph β (πΊ β ConnGraph β
(((π β π β§ 1 <
(β―βπ)) β§
(π£ β π β§ π β π£)) β βπ β ran πΌ π β π))) |
31 | 30 | pm2.43i 52 |
. . . . . 6
β’ (πΊ β ConnGraph β
(((π β π β§ 1 <
(β―βπ)) β§
(π£ β π β§ π β π£)) β βπ β ran πΌ π β π)) |
32 | 31 | expd 416 |
. . . . 5
β’ (πΊ β ConnGraph β ((π β π β§ 1 < (β―βπ)) β ((π£ β π β§ π β π£) β βπ β ran πΌ π β π))) |
33 | 32 | 3impib 1116 |
. . . 4
β’ ((πΊ β ConnGraph β§ π β π β§ 1 < (β―βπ)) β ((π£ β π β§ π β π£) β βπ β ran πΌ π β π)) |
34 | 33 | expd 416 |
. . 3
β’ ((πΊ β ConnGraph β§ π β π β§ 1 < (β―βπ)) β (π£ β π β (π β π£ β βπ β ran πΌ π β π))) |
35 | 34 | rexlimdv 3153 |
. 2
β’ ((πΊ β ConnGraph β§ π β π β§ 1 < (β―βπ)) β (βπ£ β π π β π£ β βπ β ran πΌ π β π)) |
36 | 6, 35 | mpd 15 |
1
β’ ((πΊ β ConnGraph β§ π β π β§ 1 < (β―βπ)) β βπ β ran πΌ π β π) |