Metamath Proof Explorer

Theorem midwwlks2s3

Description: There is a vertex between the endpoints of a walk of length 2 between two vertices as length 3 string. (Contributed by AV, 10-Jan-2022)

Ref Expression
Hypothesis elwwlks2s3.v ⊢ V = Vtx ⁡ G
Assertion midwwlks2s3 ⊢ W ∈ 2 WWalksN G → ∃ b ∈ V W ⁡ 1 = b

Proof

Step Hyp Ref Expression
1 elwwlks2s3.v ⊢ V = Vtx ⁡ G
2 1 elwwlks2s3 ⊢ W ∈ 2 WWalksN G → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V W = ⟨“ abc ”⟩
3 fveq1 ⊢ W = ⟨“ abc ”⟩ → W ⁡ 1 = ⟨“ abc ”⟩ ⁡ 1
4 s3fv1 ⊢ b ∈ V → ⟨“ abc ”⟩ ⁡ 1 = b
5 3 4 sylan9eqr ⊢ b ∈ V ∧ W = ⟨“ abc ”⟩ → W ⁡ 1 = b
6 5 ex ⊢ b ∈ V → W = ⟨“ abc ”⟩ → W ⁡ 1 = b
7 6 adantl ⊢ a ∈ V ∧ b ∈ V → W = ⟨“ abc ”⟩ → W ⁡ 1 = b
8 7 rexlimdvw ⊢ a ∈ V ∧ b ∈ V → ∃ c ∈ V W = ⟨“ abc ”⟩ → W ⁡ 1 = b
9 8 reximdva ⊢ a ∈ V → ∃ b ∈ V ∃ c ∈ V W = ⟨“ abc ”⟩ → ∃ b ∈ V W ⁡ 1 = b
10 9 rexlimiv ⊢ ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V W = ⟨“ abc ”⟩ → ∃ b ∈ V W ⁡ 1 = b
11 2 10 syl ⊢ W ∈ 2 WWalksN G → ∃ b ∈ V W ⁡ 1 = b