Theorem wwlksnon0

Description: Sufficient conditions for a set of walks of a fixed length between two vertices to be empty. (Contributed by AV, 15-May-2021) (Proof shortened by AV, 21-May-2021)

	Ref	Expression
Hypothesis	wwlksnon0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	wwlksnon0	⊢ ( ¬ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		wwlksnon0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		df-wwlksnon	⊢ WWalksNOn = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑛 ) = 𝑏 ) } ) )
3	1	wwlksnon	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 WWalksNOn 𝐺 ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } ) )
4	2 3	2mpo0	⊢ ( ¬ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) = ∅ )