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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
fusgreg2wsp.m ⊢ 𝑀 = ( 𝑎 ∈ 𝑉 ↦ { 𝑤 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑤 ‘ 1 ) = 𝑎 } )
Assertion fusgreg2wsp ( 𝐺 ∈ FinUSGraph → ( 2 WSPathsN 𝐺 ) = ∪ 𝑥 ∈ 𝑉 ( 𝑀 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 frgrhash2wsp.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 fusgreg2wsp.m ⊢ 𝑀 = ( 𝑎 ∈ 𝑉 ↦ { 𝑤 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑤 ‘ 1 ) = 𝑎 } )
3 wspthsswwlkn ⊢ ( 2 WSPathsN 𝐺 ) ⊆ ( 2 WWalksN 𝐺 )
4 3 sseli ⊢ ( 𝑝 ∈ ( 2 WSPathsN 𝐺 ) → 𝑝 ∈ ( 2 WWalksN 𝐺 ) )
5 1 midwwlks2s3 ⊢ ( 𝑝 ∈ ( 2 WWalksN 𝐺 ) → ∃ 𝑥 ∈ 𝑉 ( 𝑝 ‘ 1 ) = 𝑥 )
6 4 5 syl ⊢ ( 𝑝 ∈ ( 2 WSPathsN 𝐺 ) → ∃ 𝑥 ∈ 𝑉 ( 𝑝 ‘ 1 ) = 𝑥 )
7 6 a1i ⊢ ( 𝐺 ∈ FinUSGraph → ( 𝑝 ∈ ( 2 WSPathsN 𝐺 ) → ∃ 𝑥 ∈ 𝑉 ( 𝑝 ‘ 1 ) = 𝑥 ) )
8 7 pm4.71rd ⊢ ( 𝐺 ∈ FinUSGraph → ( 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ↔ ( ∃ 𝑥 ∈ 𝑉 ( 𝑝 ‘ 1 ) = 𝑥 ∧ 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ) ) )
9 ancom ⊢ ( ( 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑝 ‘ 1 ) = 𝑥 ) ↔ ( ( 𝑝 ‘ 1 ) = 𝑥 ∧ 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ) )
10 9 rexbii ⊢ ( ∃ 𝑥 ∈ 𝑉 ( 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑝 ‘ 1 ) = 𝑥 ) ↔ ∃ 𝑥 ∈ 𝑉 ( ( 𝑝 ‘ 1 ) = 𝑥 ∧ 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ) )
11 r19.41v ⊢ ( ∃ 𝑥 ∈ 𝑉 ( ( 𝑝 ‘ 1 ) = 𝑥 ∧ 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ) ↔ ( ∃ 𝑥 ∈ 𝑉 ( 𝑝 ‘ 1 ) = 𝑥 ∧ 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ) )
12 10 11 bitr2i ⊢ ( ( ∃ 𝑥 ∈ 𝑉 ( 𝑝 ‘ 1 ) = 𝑥 ∧ 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ) ↔ ∃ 𝑥 ∈ 𝑉 ( 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑝 ‘ 1 ) = 𝑥 ) )
13 12 a1i ⊢ ( 𝐺 ∈ FinUSGraph → ( ( ∃ 𝑥 ∈ 𝑉 ( 𝑝 ‘ 1 ) = 𝑥 ∧ 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ) ↔ ∃ 𝑥 ∈ 𝑉 ( 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑝 ‘ 1 ) = 𝑥 ) ) )
14 1 2 fusgreg2wsplem ⊢ ( 𝑥 ∈ 𝑉 → ( 𝑝 ∈ ( 𝑀 ‘ 𝑥 ) ↔ ( 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑝 ‘ 1 ) = 𝑥 ) ) )
15 14 bicomd ⊢ ( 𝑥 ∈ 𝑉 → ( ( 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑝 ‘ 1 ) = 𝑥 ) ↔ 𝑝 ∈ ( 𝑀 ‘ 𝑥 ) ) )
16 15 adantl ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑝 ‘ 1 ) = 𝑥 ) ↔ 𝑝 ∈ ( 𝑀 ‘ 𝑥 ) ) )
17 16 rexbidva ⊢ ( 𝐺 ∈ FinUSGraph → ( ∃ 𝑥 ∈ 𝑉 ( 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ∧ ( 𝑝 ‘ 1 ) = 𝑥 ) ↔ ∃ 𝑥 ∈ 𝑉 𝑝 ∈ ( 𝑀 ‘ 𝑥 ) ) )
18 8 13 17 3bitrd ⊢ ( 𝐺 ∈ FinUSGraph → ( 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ↔ ∃ 𝑥 ∈ 𝑉 𝑝 ∈ ( 𝑀 ‘ 𝑥 ) ) )
19 eliun ⊢ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝑉 ( 𝑀 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝑉 𝑝 ∈ ( 𝑀 ‘ 𝑥 ) )
20 18 19 bitr4di ⊢ ( 𝐺 ∈ FinUSGraph → ( 𝑝 ∈ ( 2 WSPathsN 𝐺 ) ↔ 𝑝 ∈ ∪ 𝑥 ∈ 𝑉 ( 𝑀 ‘ 𝑥 ) ) )
21 20 eqrdv ⊢ ( 𝐺 ∈ FinUSGraph → ( 2 WSPathsN 𝐺 ) = ∪ 𝑥 ∈ 𝑉 ( 𝑀 ‘ 𝑥 ) )