Step | Hyp | Ref
| Expression |
1 | | conngrv2edg.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | fvex 6113 |
. . . 4
⊢
(Vtx‘𝐺) ∈
V |
3 | 1, 2 | eqeltri 2684 |
. . 3
⊢ 𝑉 ∈ V |
4 | | simp3 1056 |
. . 3
⊢ ((𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) → 1 < (#‘𝑉)) |
5 | | simp2 1055 |
. . 3
⊢ ((𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) → 𝑁 ∈ 𝑉) |
6 | | hashgt12el2 13071 |
. . 3
⊢ ((𝑉 ∈ V ∧ 1 <
(#‘𝑉) ∧ 𝑁 ∈ 𝑉) → ∃𝑣 ∈ 𝑉 𝑁 ≠ 𝑣) |
7 | 3, 4, 5, 6 | mp3an2i 1421 |
. 2
⊢ ((𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) → ∃𝑣 ∈ 𝑉 𝑁 ≠ 𝑣) |
8 | 1 | isconngr 41356 |
. . . . . . . 8
⊢ (𝐺 ∈ ConnGraph → (𝐺 ∈ ConnGraph ↔
∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑓∃𝑝 𝑓(𝑎(PathsOn‘𝐺)𝑏)𝑝)) |
9 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑁 → (𝑎(PathsOn‘𝐺)𝑏) = (𝑁(PathsOn‘𝐺)𝑏)) |
10 | 9 | breqd 4594 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑁 → (𝑓(𝑎(PathsOn‘𝐺)𝑏)𝑝 ↔ 𝑓(𝑁(PathsOn‘𝐺)𝑏)𝑝)) |
11 | 10 | 2exbidv 1839 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑁 → (∃𝑓∃𝑝 𝑓(𝑎(PathsOn‘𝐺)𝑏)𝑝 ↔ ∃𝑓∃𝑝 𝑓(𝑁(PathsOn‘𝐺)𝑏)𝑝)) |
12 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑣 → (𝑁(PathsOn‘𝐺)𝑏) = (𝑁(PathsOn‘𝐺)𝑣)) |
13 | 12 | breqd 4594 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑣 → (𝑓(𝑁(PathsOn‘𝐺)𝑏)𝑝 ↔ 𝑓(𝑁(PathsOn‘𝐺)𝑣)𝑝)) |
14 | 13 | 2exbidv 1839 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑣 → (∃𝑓∃𝑝 𝑓(𝑁(PathsOn‘𝐺)𝑏)𝑝 ↔ ∃𝑓∃𝑝 𝑓(𝑁(PathsOn‘𝐺)𝑣)𝑝)) |
15 | 11, 14 | rspc2v 3293 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉) → (∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑓∃𝑝 𝑓(𝑎(PathsOn‘𝐺)𝑏)𝑝 → ∃𝑓∃𝑝 𝑓(𝑁(PathsOn‘𝐺)𝑣)𝑝)) |
16 | 15 | ad2ant2r 779 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) ∧ (𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣)) → (∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑓∃𝑝 𝑓(𝑎(PathsOn‘𝐺)𝑏)𝑝 → ∃𝑓∃𝑝 𝑓(𝑁(PathsOn‘𝐺)𝑣)𝑝)) |
17 | | pthontrlon 40953 |
. . . . . . . . . . . . 13
⊢ (𝑓(𝑁(PathsOn‘𝐺)𝑣)𝑝 → 𝑓(𝑁(TrailsOn‘𝐺)𝑣)𝑝) |
18 | | trlsonwlkon 40917 |
. . . . . . . . . . . . 13
⊢ (𝑓(𝑁(TrailsOn‘𝐺)𝑣)𝑝 → 𝑓(𝑁(WalksOn‘𝐺)𝑣)𝑝) |
19 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓(𝑁(WalksOn‘𝐺)𝑣)𝑝 ∧ ((𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) ∧ (𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣))) → 𝑓(𝑁(WalksOn‘𝐺)𝑣)𝑝) |
20 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) ∧ (𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣)) → 𝑁 ≠ 𝑣) |
21 | | wlkOn2n0 40874 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓(𝑁(WalksOn‘𝐺)𝑣)𝑝 ∧ 𝑁 ≠ 𝑣) → (#‘𝑓) ≠ 0) |
22 | 20, 21 | sylan2 490 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓(𝑁(WalksOn‘𝐺)𝑣)𝑝 ∧ ((𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) ∧ (𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣))) → (#‘𝑓) ≠ 0) |
23 | 19, 22 | jca 553 |
. . . . . . . . . . . . . 14
⊢ ((𝑓(𝑁(WalksOn‘𝐺)𝑣)𝑝 ∧ ((𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) ∧ (𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣))) → (𝑓(𝑁(WalksOn‘𝐺)𝑣)𝑝 ∧ (#‘𝑓) ≠ 0)) |
24 | 23 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑓(𝑁(WalksOn‘𝐺)𝑣)𝑝 → (((𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) ∧ (𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣)) → (𝑓(𝑁(WalksOn‘𝐺)𝑣)𝑝 ∧ (#‘𝑓) ≠ 0))) |
25 | 17, 18, 24 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝑓(𝑁(PathsOn‘𝐺)𝑣)𝑝 → (((𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) ∧ (𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣)) → (𝑓(𝑁(WalksOn‘𝐺)𝑣)𝑝 ∧ (#‘𝑓) ≠ 0))) |
26 | | conngrv2edg.i |
. . . . . . . . . . . . 13
⊢ 𝐼 = (iEdg‘𝐺) |
27 | 26 | wlkOnl1iedg 40873 |
. . . . . . . . . . . 12
⊢ ((𝑓(𝑁(WalksOn‘𝐺)𝑣)𝑝 ∧ (#‘𝑓) ≠ 0) → ∃𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒) |
28 | 25, 27 | syl6com 36 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) ∧ (𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣)) → (𝑓(𝑁(PathsOn‘𝐺)𝑣)𝑝 → ∃𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒)) |
29 | 28 | exlimdvv 1849 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) ∧ (𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣)) → (∃𝑓∃𝑝 𝑓(𝑁(PathsOn‘𝐺)𝑣)𝑝 → ∃𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒)) |
30 | 16, 29 | syld 46 |
. . . . . . . . 9
⊢ (((𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) ∧ (𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣)) → (∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑓∃𝑝 𝑓(𝑎(PathsOn‘𝐺)𝑏)𝑝 → ∃𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒)) |
31 | 30 | com12 32 |
. . . . . . . 8
⊢
(∀𝑎 ∈
𝑉 ∀𝑏 ∈ 𝑉 ∃𝑓∃𝑝 𝑓(𝑎(PathsOn‘𝐺)𝑏)𝑝 → (((𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) ∧ (𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣)) → ∃𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒)) |
32 | 8, 31 | syl6bi 242 |
. . . . . . 7
⊢ (𝐺 ∈ ConnGraph → (𝐺 ∈ ConnGraph →
(((𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) ∧ (𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣)) → ∃𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒))) |
33 | 32 | pm2.43i 50 |
. . . . . 6
⊢ (𝐺 ∈ ConnGraph →
(((𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) ∧ (𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣)) → ∃𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒)) |
34 | 33 | expd 451 |
. . . . 5
⊢ (𝐺 ∈ ConnGraph → ((𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) → ((𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣) → ∃𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒))) |
35 | 34 | 3impib 1254 |
. . . 4
⊢ ((𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) → ((𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣) → ∃𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒)) |
36 | 35 | expd 451 |
. . 3
⊢ ((𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) → (𝑣 ∈ 𝑉 → (𝑁 ≠ 𝑣 → ∃𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒))) |
37 | 36 | rexlimdv 3012 |
. 2
⊢ ((𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) → (∃𝑣 ∈ 𝑉 𝑁 ≠ 𝑣 → ∃𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒)) |
38 | 7, 37 | mpd 15 |
1
⊢ ((𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < (#‘𝑉)) → ∃𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒) |