Theorem wspthnonp

Description: Properties of a set being a simple path of a fixed length between two vertices as word. (Contributed by AV, 14-May-2021) (Proof shortened by AV, 15-Mar-2022)

	Ref	Expression
Hypothesis	wspthnonp.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	wspthnonp	⊢ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		wspthnonp.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		fvex	⊢ ( Vtx ‘ 𝑔 ) ∈ V
3	2 2	pm3.2i	⊢ ( ( Vtx ‘ 𝑔 ) ∈ V ∧ ( Vtx ‘ 𝑔 ) ∈ V )
4	3	rgen2w	⊢ ∀ 𝑛 ∈ ℕ0 ∀ 𝑔 ∈ V ( ( Vtx ‘ 𝑔 ) ∈ V ∧ ( Vtx ‘ 𝑔 ) ∈ V )
5		df-wspthsnon	⊢ WSPathsNOn = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 } ) )
6		fveq2	⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
7	6 6	jca	⊢ ( 𝑔 = 𝐺 → ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ) )
8	7	adantl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ) )
9	5 8	el2mpocl	⊢ ( ∀ 𝑛 ∈ ℕ0 ∀ 𝑔 ∈ V ( ( Vtx ‘ 𝑔 ) ∈ V ∧ ( Vtx ‘ 𝑔 ) ∈ V ) → ( 𝑊 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ) )
10	4 9	ax-mp	⊢ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) )
11		simprl	⊢ ( ( 𝑊 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) ∧ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ) → ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) )
12	1	eleq2i	⊢ ( 𝐴 ∈ 𝑉 ↔ 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
13	1	eleq2i	⊢ ( 𝐵 ∈ 𝑉 ↔ 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
14	12 13	anbi12i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ↔ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) )
15	14	bilanri	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
16	15	adantl	⊢ ( ( 𝑊 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) ∧ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
17		wspthnon	⊢ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) ↔ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑊 ) )
18	17	birani	⊢ ( ( 𝑊 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) ∧ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ) → ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑊 ) )
19	11 16 18	3jca	⊢ ( ( 𝑊 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) ∧ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑊 ) ) )
20	10 19	mpdan	⊢ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑊 ) ) )