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 𝐼 𝐴 ∈ 𝑒 )