This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimpri ⊢ ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
16 15 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
17 16 adantl ⊢ ( ( 𝑊 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) ∧ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
18 wspthnon ⊢ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) ↔ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑊 ) )
19 18 biimpi ⊢ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) → ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑊 ) )
20 19 adantr ⊢ ( ( 𝑊 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) ∧ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ) → ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑊 ) )
21 11 17 20 3jca ⊢ ( ( 𝑊 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) ∧ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑊 ) ) )
22 10 21 mpdan ⊢ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑊 ) ) )