Metamath Proof Explorer

Theorem 2wspiundisj

Description: All simple paths of length 2 from a fixed vertex to another vertex are disjunct. (Contributed by Alexander van der Vekens, 5-Mar-2018) (Revised by AV, 14-May-2021) (Proof shortened by AV, 9-Jan-2022)

Ref Expression
Assertion 2wspiundisj ⊢ Disj a ∈ V ⋃ b ∈ V ∖ a a 2 WSPathsNOn G b

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ a = c → a 2 WSPathsNOn G b = c 2 WSPathsNOn G b
2 oveq2 ⊢ b = d → c 2 WSPathsNOn G b = c 2 WSPathsNOn G d
3 sneq ⊢ a = c → a = c
4 3 difeq2d ⊢ a = c → V ∖ a = V ∖ c
5 wspthneq1eq2 ⊢ t ∈ a 2 WSPathsNOn G b ∧ t ∈ c 2 WSPathsNOn G d → a = c ∧ b = d
6 5 simpld ⊢ t ∈ a 2 WSPathsNOn G b ∧ t ∈ c 2 WSPathsNOn G d → a = c
7 6 3adant1 ⊢ ⊤ ∧ t ∈ a 2 WSPathsNOn G b ∧ t ∈ c 2 WSPathsNOn G d → a = c
8 1 2 4 7 disjiund ⊢ ⊤ → Disj a ∈ V ⋃ b ∈ V ∖ a a 2 WSPathsNOn G b
9 8 mptru ⊢ Disj a ∈ V ⋃ b ∈ V ∖ a a 2 WSPathsNOn G b