Metamath Proof Explorer

Theorem elwwlks2on

Description: A walk of length 2 between two vertices as length 3 string. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 12-May-2021)

Ref Expression
Hypothesis elwwlks2on.v ⊢ V = Vtx ⁡ G
Assertion elwwlks2on ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → W ∈ A 2 WWalksNOn G C ↔ ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ∃ f f Walks ⁡ G W ∧ f = 2

Proof

Step Hyp Ref Expression
1 elwwlks2on.v ⊢ V = Vtx ⁡ G
2 1 elwwlks2ons3 ⊢ W ∈ A 2 WWalksNOn G C ↔ ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C
3 1 s3wwlks2on ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C ↔ ∃ f f Walks ⁡ G ⟨“ AbC ”⟩ ∧ f = 2
4 breq2 ⊢ ⟨“ AbC ”⟩ = W → f Walks ⁡ G ⟨“ AbC ”⟩ ↔ f Walks ⁡ G W
5 4 eqcoms ⊢ W = ⟨“ AbC ”⟩ → f Walks ⁡ G ⟨“ AbC ”⟩ ↔ f Walks ⁡ G W
6 5 anbi1d ⊢ W = ⟨“ AbC ”⟩ → f Walks ⁡ G ⟨“ AbC ”⟩ ∧ f = 2 ↔ f Walks ⁡ G W ∧ f = 2
7 6 exbidv ⊢ W = ⟨“ AbC ”⟩ → ∃ f f Walks ⁡ G ⟨“ AbC ”⟩ ∧ f = 2 ↔ ∃ f f Walks ⁡ G W ∧ f = 2
8 3 7 sylan9bb ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V ∧ W = ⟨“ AbC ”⟩ → ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C ↔ ∃ f f Walks ⁡ G W ∧ f = 2
9 8 pm5.32da ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C ↔ W = ⟨“ AbC ”⟩ ∧ ∃ f f Walks ⁡ G W ∧ f = 2
10 9 rexbidv ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C ↔ ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ∃ f f Walks ⁡ G W ∧ f = 2
11 2 10 bitrid ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → W ∈ A 2 WWalksNOn G C ↔ ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ∃ f f Walks ⁡ G W ∧ f = 2