Metamath Proof Explorer

Theorem rusgr0edg

Description: Special case for graphs without edges: There are no walks of length greater than 0. (Contributed by Alexander van der Vekens, 26-Jul-2018) (Revised by AV, 7-May-2021)

Ref Expression
Hypotheses rusgrnumwwlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
rusgrnumwwlk.l ⊢ 𝐿 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ0 ↦ ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )
Assertion rusgr0edg ( ( 𝐺 RegUSGraph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑃 𝐿 𝑁 ) = 0 )

Proof

Step Hyp Ref Expression
1 rusgrnumwwlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 rusgrnumwwlk.l ⊢ 𝐿 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ0 ↦ ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )
3 simp2 ⊢ ( ( 𝐺 RegUSGraph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → 𝑃 ∈ 𝑉 )
4 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
5 4 3ad2ant3 ⊢ ( ( 𝐺 RegUSGraph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
6 1 2 rusgrnumwwlklem ⊢ ( ( 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑃 𝐿 𝑁 ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) )
7 3 5 6 syl2anc ⊢ ( ( 𝐺 RegUSGraph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑃 𝐿 𝑁 ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) )
8 rusgrusgr ⊢ ( 𝐺 RegUSGraph 0 → 𝐺 ∈ USGraph )
9 usgr0edg0rusgr ⊢ ( 𝐺 ∈ USGraph → ( 𝐺 RegUSGraph 0 ↔ ( Edg ‘ 𝐺 ) = ∅ ) )
10 9 biimpcd ⊢ ( 𝐺 RegUSGraph 0 → ( 𝐺 ∈ USGraph → ( Edg ‘ 𝐺 ) = ∅ ) )
11 8 10 mpd ⊢ ( 𝐺 RegUSGraph 0 → ( Edg ‘ 𝐺 ) = ∅ )
12 0enwwlksnge1 ⊢ ( ( ( Edg ‘ 𝐺 ) = ∅ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 WWalksN 𝐺 ) = ∅ )
13 11 12 sylan ⊢ ( ( 𝐺 RegUSGraph 0 ∧ 𝑁 ∈ ℕ ) → ( 𝑁 WWalksN 𝐺 ) = ∅ )
14 eleq2 ⊢ ( ( 𝑁 WWalksN 𝐺 ) = ∅ → ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ 𝑤 ∈ ∅ ) )
15 noel ⊢ ¬ 𝑤 ∈ ∅
16 15 pm2.21i ⊢ ( 𝑤 ∈ ∅ → ¬ ( 𝑤 ‘ 0 ) = 𝑃 )
17 14 16 biimtrdi ⊢ ( ( 𝑁 WWalksN 𝐺 ) = ∅ → ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ¬ ( 𝑤 ‘ 0 ) = 𝑃 ) )
18 13 17 syl ⊢ ( ( 𝐺 RegUSGraph 0 ∧ 𝑁 ∈ ℕ ) → ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ¬ ( 𝑤 ‘ 0 ) = 𝑃 ) )
19 18 3adant2 ⊢ ( ( 𝐺 RegUSGraph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ¬ ( 𝑤 ‘ 0 ) = 𝑃 ) )
20 19 ralrimiv ⊢ ( ( 𝐺 RegUSGraph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ∀ 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ¬ ( 𝑤 ‘ 0 ) = 𝑃 )
21 rabeq0 ⊢ ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } = ∅ ↔ ∀ 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ¬ ( 𝑤 ‘ 0 ) = 𝑃 )
22 20 21 sylibr ⊢ ( ( 𝐺 RegUSGraph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } = ∅ )
23 22 fveq2d ⊢ ( ( 𝐺 RegUSGraph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( ♯ ‘ ∅ ) )
24 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
25 23 24 eqtrdi ⊢ ( ( 𝐺 RegUSGraph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = 0 )
26 7 25 eqtrd ⊢ ( ( 𝐺 RegUSGraph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑃 𝐿 𝑁 ) = 0 )