Metamath Proof Explorer

Theorem fusgreg2wsp

Description: In a finite simple graph, the set of all paths of length 2 is the union of all the paths of length 2 over the vertices which are in the middle of such a path. (Contributed by Alexander van der Vekens, 10-Mar-2018) (Revised by AV, 18-May-2021) (Proof shortened by AV, 10-Jan-2022)

Ref Expression
Hypotheses frgrhash2wsp.v ⊢ V = Vtx ⁡ G
fusgreg2wsp.m ⊢ M = a ∈ V ⟼ w ∈ 2 WSPathsN G | w ⁡ 1 = a
Assertion fusgreg2wsp ⊢ G ∈ FinUSGraph → 2 WSPathsN G = ⋃ x ∈ V M ⁡ x

Proof

Step Hyp Ref Expression
1 frgrhash2wsp.v ⊢ V = Vtx ⁡ G
2 fusgreg2wsp.m ⊢ M = a ∈ V ⟼ w ∈ 2 WSPathsN G | w ⁡ 1 = a
3 wspthsswwlkn ⊢ 2 WSPathsN G ⊆ 2 WWalksN G
4 3 sseli ⊢ p ∈ 2 WSPathsN G → p ∈ 2 WWalksN G
5 1 midwwlks2s3 ⊢ p ∈ 2 WWalksN G → ∃ x ∈ V p ⁡ 1 = x
6 4 5 syl ⊢ p ∈ 2 WSPathsN G → ∃ x ∈ V p ⁡ 1 = x
7 6 a1i ⊢ G ∈ FinUSGraph → p ∈ 2 WSPathsN G → ∃ x ∈ V p ⁡ 1 = x
8 7 pm4.71rd ⊢ G ∈ FinUSGraph → p ∈ 2 WSPathsN G ↔ ∃ x ∈ V p ⁡ 1 = x ∧ p ∈ 2 WSPathsN G
9 ancom ⊢ p ∈ 2 WSPathsN G ∧ p ⁡ 1 = x ↔ p ⁡ 1 = x ∧ p ∈ 2 WSPathsN G
10 9 rexbii ⊢ ∃ x ∈ V p ∈ 2 WSPathsN G ∧ p ⁡ 1 = x ↔ ∃ x ∈ V p ⁡ 1 = x ∧ p ∈ 2 WSPathsN G
11 r19.41v ⊢ ∃ x ∈ V p ⁡ 1 = x ∧ p ∈ 2 WSPathsN G ↔ ∃ x ∈ V p ⁡ 1 = x ∧ p ∈ 2 WSPathsN G
12 10 11 bitr2i ⊢ ∃ x ∈ V p ⁡ 1 = x ∧ p ∈ 2 WSPathsN G ↔ ∃ x ∈ V p ∈ 2 WSPathsN G ∧ p ⁡ 1 = x
13 12 a1i ⊢ G ∈ FinUSGraph → ∃ x ∈ V p ⁡ 1 = x ∧ p ∈ 2 WSPathsN G ↔ ∃ x ∈ V p ∈ 2 WSPathsN G ∧ p ⁡ 1 = x
14 1 2 fusgreg2wsplem ⊢ x ∈ V → p ∈ M ⁡ x ↔ p ∈ 2 WSPathsN G ∧ p ⁡ 1 = x
15 14 bicomd ⊢ x ∈ V → p ∈ 2 WSPathsN G ∧ p ⁡ 1 = x ↔ p ∈ M ⁡ x
16 15 adantl ⊢ G ∈ FinUSGraph ∧ x ∈ V → p ∈ 2 WSPathsN G ∧ p ⁡ 1 = x ↔ p ∈ M ⁡ x
17 16 rexbidva ⊢ G ∈ FinUSGraph → ∃ x ∈ V p ∈ 2 WSPathsN G ∧ p ⁡ 1 = x ↔ ∃ x ∈ V p ∈ M ⁡ x
18 8 13 17 3bitrd ⊢ G ∈ FinUSGraph → p ∈ 2 WSPathsN G ↔ ∃ x ∈ V p ∈ M ⁡ x
19 eliun ⊢ p ∈ ⋃ x ∈ V M ⁡ x ↔ ∃ x ∈ V p ∈ M ⁡ x
20 18 19 bitr4di ⊢ G ∈ FinUSGraph → p ∈ 2 WSPathsN G ↔ p ∈ ⋃ x ∈ V M ⁡ x
21 20 eqrdv ⊢ G ∈ FinUSGraph → 2 WSPathsN G = ⋃ x ∈ V M ⁡ x