Metamath Proof Explorer

Theorem trlsonfval

Description: The set of trails between two vertices. (Contributed by Alexander van der Vekens, 4-Nov-2017) (Revised by AV, 7-Jan-2021) (Proof shortened by AV, 15-Jan-2021) (Revised by AV, 21-Mar-2021)

Ref Expression
Hypothesis trlsonfval.v ⊢ V = Vtx ⁡ G
Assertion trlsonfval ⊢ A ∈ V ∧ B ∈ V → A TrailsOn ⁡ G B = f p | f A WalksOn ⁡ G B p ∧ f Trails ⁡ G p

Proof

Step Hyp Ref Expression
1 trlsonfval.v ⊢ V = Vtx ⁡ G
2 1 1vgrex ⊢ A ∈ V → G ∈ V
3 2 adantr ⊢ A ∈ V ∧ B ∈ V → G ∈ V
4 simpl ⊢ A ∈ V ∧ B ∈ V → A ∈ V
5 4 1 eleqtrdi ⊢ A ∈ V ∧ B ∈ V → A ∈ Vtx ⁡ G
6 simpr ⊢ A ∈ V ∧ B ∈ V → B ∈ V
7 6 1 eleqtrdi ⊢ A ∈ V ∧ B ∈ V → B ∈ Vtx ⁡ G
8 wksv ⊢ f p | f Walks ⁡ G p ∈ V
9 8 a1i ⊢ A ∈ V ∧ B ∈ V → f p | f Walks ⁡ G p ∈ V
10 trliswlk ⊢ f Trails ⁡ G p → f Walks ⁡ G p
11 10 adantl ⊢ A ∈ V ∧ B ∈ V ∧ f Trails ⁡ G p → f Walks ⁡ G p
12 df-trlson ⊢ TrailsOn = g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f a WalksOn ⁡ g b p ∧ f Trails ⁡ g p
13 3 5 7 9 11 12 mptmpoopabovd ⊢ A ∈ V ∧ B ∈ V → A TrailsOn ⁡ G B = f p | f A WalksOn ⁡ G B p ∧ f Trails ⁡ G p