Metamath Proof Explorer


Theorem wlkonl1iedg

Description: If there is a walk between two vertices A and B at least of length 1, then the start vertex A is incident with an edge. (Contributed by AV, 4-Apr-2021)

Ref Expression
Hypothesis wlkonl1iedg.i 𝐼 = ( iEdg ‘ 𝐺 )
Assertion wlkonl1iedg ( ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) ≠ 0 ) → ∃ 𝑒 ∈ ran 𝐼 𝐴𝑒 )

Proof

Step Hyp Ref Expression
1 wlkonl1iedg.i 𝐼 = ( iEdg ‘ 𝐺 )
2 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 2 wlkonprop ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )
4 fveq2 ( 𝑘 = 0 → ( 𝑃𝑘 ) = ( 𝑃 ‘ 0 ) )
5 fv0p1e1 ( 𝑘 = 0 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 1 ) )
6 4 5 preq12d ( 𝑘 = 0 → { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
7 6 sseq1d ( 𝑘 = 0 → ( { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ 𝑒 ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ 𝑒 ) )
8 7 rexbidv ( 𝑘 = 0 → ( ∃ 𝑒 ∈ ran 𝐼 { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ ran 𝐼 { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ 𝑒 ) )
9 1 wlkvtxiedg ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∃ 𝑒 ∈ ran 𝐼 { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ 𝑒 )
10 9 adantr ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∃ 𝑒 ∈ ran 𝐼 { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ 𝑒 )
11 10 adantr ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ) ∧ ( ♯ ‘ 𝐹 ) ≠ 0 ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∃ 𝑒 ∈ ran 𝐼 { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ 𝑒 )
12 wlkcl ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
13 elnnne0 ( ( ♯ ‘ 𝐹 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ≠ 0 ) )
14 13 simplbi2 ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐹 ) ≠ 0 → ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
15 lbfzo0 ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( ♯ ‘ 𝐹 ) ∈ ℕ )
16 14 15 syl6ibr ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐹 ) ≠ 0 → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
17 12 16 syl ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) ≠ 0 → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
18 17 adantr ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ) → ( ( ♯ ‘ 𝐹 ) ≠ 0 → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
19 18 imp ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ) ∧ ( ♯ ‘ 𝐹 ) ≠ 0 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
20 8 11 19 rspcdva ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ) ∧ ( ♯ ‘ 𝐹 ) ≠ 0 ) → ∃ 𝑒 ∈ ran 𝐼 { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ 𝑒 )
21 fvex ( 𝑃 ‘ 0 ) ∈ V
22 fvex ( 𝑃 ‘ 1 ) ∈ V
23 21 22 prss ( ( ( 𝑃 ‘ 0 ) ∈ 𝑒 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑒 ) ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ 𝑒 )
24 eleq1 ( ( 𝑃 ‘ 0 ) = 𝐴 → ( ( 𝑃 ‘ 0 ) ∈ 𝑒𝐴𝑒 ) )
25 ax-1 ( 𝐴𝑒 → ( ( 𝑃 ‘ 1 ) ∈ 𝑒𝐴𝑒 ) )
26 24 25 syl6bi ( ( 𝑃 ‘ 0 ) = 𝐴 → ( ( 𝑃 ‘ 0 ) ∈ 𝑒 → ( ( 𝑃 ‘ 1 ) ∈ 𝑒𝐴𝑒 ) ) )
27 26 adantl ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ) → ( ( 𝑃 ‘ 0 ) ∈ 𝑒 → ( ( 𝑃 ‘ 1 ) ∈ 𝑒𝐴𝑒 ) ) )
28 27 impd ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ) → ( ( ( 𝑃 ‘ 0 ) ∈ 𝑒 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑒 ) → 𝐴𝑒 ) )
29 23 28 syl5bir ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ 𝑒𝐴𝑒 ) )
30 29 reximdv ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ) → ( ∃ 𝑒 ∈ ran 𝐼 { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ 𝑒 → ∃ 𝑒 ∈ ran 𝐼 𝐴𝑒 ) )
31 30 adantr ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ) ∧ ( ♯ ‘ 𝐹 ) ≠ 0 ) → ( ∃ 𝑒 ∈ ran 𝐼 { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ 𝑒 → ∃ 𝑒 ∈ ran 𝐼 𝐴𝑒 ) )
32 20 31 mpd ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ) ∧ ( ♯ ‘ 𝐹 ) ≠ 0 ) → ∃ 𝑒 ∈ ran 𝐼 𝐴𝑒 )
33 32 ex ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ) → ( ( ♯ ‘ 𝐹 ) ≠ 0 → ∃ 𝑒 ∈ ran 𝐼 𝐴𝑒 ) )
34 33 3adant3 ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( ( ♯ ‘ 𝐹 ) ≠ 0 → ∃ 𝑒 ∈ ran 𝐼 𝐴𝑒 ) )
35 34 3ad2ant3 ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( ( ♯ ‘ 𝐹 ) ≠ 0 → ∃ 𝑒 ∈ ran 𝐼 𝐴𝑒 ) )
36 3 35 syl ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) ≠ 0 → ∃ 𝑒 ∈ ran 𝐼 𝐴𝑒 ) )
37 36 imp ( ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) ≠ 0 ) → ∃ 𝑒 ∈ ran 𝐼 𝐴𝑒 )