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

Metamath Proof Explorer

Theorem wlkv

Description: The classes involved in a walk are sets. (Contributed by Alexander van der Vekens, 31-Oct-2017) (Revised by AV, 3-Feb-2021)

Ref Expression
Assertion wlkv ⊢ F Walks ⁡ G P → G ∈ V ∧ F ∈ V ∧ P ∈ V

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
3 1 2 wksfval ⊢ G ∈ V → Walks ⁡ G = f p | f ∈ Word dom ⁡ iEdg ⁡ G ∧ p : 0 … f ⟶ Vtx ⁡ G ∧ ∀ k ∈ 0 ..^ f if- p ⁡ k = p ⁡ k + 1 iEdg ⁡ G ⁡ f ⁡ k = p ⁡ k p ⁡ k p ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ f ⁡ k
4 3 brfvopab ⊢ F Walks ⁡ G P → G ∈ V ∧ F ∈ V ∧ P ∈ V