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

Metamath Proof Explorer

Theorem wlkonprop

Description: Properties of a walk between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017) (Revised by AV, 31-Dec-2020) (Proof shortened by AV, 16-Jan-2021)

Ref Expression
Hypothesis wlkson.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion wlkonprop ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 wlkson.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 fvexi ⊢ 𝑉 ∈ V
3 df-wlkson ⊢ WalksOn = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) } ) )
4 1 wlkson ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) } )
5 4 3adant1 ⊢ ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) } )
6 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
7 6 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 )
8 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Walks ‘ 𝑔 ) = ( Walks ‘ 𝐺 ) )
9 8 breqd ⊢ ( 𝑔 = 𝐺 → ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ↔ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) )
10 9 3anbi1d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ) )
11 3 5 7 7 10 bropfvvvv ⊢ ( ( 𝑉 ∈ V ∧ 𝑉 ∈ V ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( 𝐺 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) )
12 2 2 11 mp2an ⊢ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( 𝐺 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
13 3anass ⊢ ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ↔ ( 𝐺 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) )
14 13 anbi1i ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ↔ ( ( 𝐺 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
15 df-3an ⊢ ( ( 𝐺 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ↔ ( ( 𝐺 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
16 14 15 bitr4i ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ↔ ( 𝐺 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
17 12 16 sylibr ⊢ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
18 1 iswlkon ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )
19 18 3adantl1 ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )
20 19 biimpd ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )
21 20 imdistani ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ∧ 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ) → ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )
22 17 21 mpancom ⊢ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )
23 df-3an ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) ↔ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )
24 22 23 sylibr ⊢ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )