This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ( 𝑎 ( 2 WSPathsNOn 𝐺 ) 𝑏 )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 ( 2 WSPathsNOn 𝐺 ) 𝑏 ) = ( 𝑐 ( 2 WSPathsNOn 𝐺 ) 𝑏 ) )
2 oveq2 ⊢ ( 𝑏 = 𝑑 → ( 𝑐 ( 2 WSPathsNOn 𝐺 ) 𝑏 ) = ( 𝑐 ( 2 WSPathsNOn 𝐺 ) 𝑑 ) )
3 sneq ⊢ ( 𝑎 = 𝑐 → { 𝑎 } = { 𝑐 } )
4 3 difeq2d ⊢ ( 𝑎 = 𝑐 → ( 𝑉 ∖ { 𝑎 } ) = ( 𝑉 ∖ { 𝑐 } ) )
5 wspthneq1eq2 ⊢ ( ( 𝑡 ∈ ( 𝑎 ( 2 WSPathsNOn 𝐺 ) 𝑏 ) ∧ 𝑡 ∈ ( 𝑐 ( 2 WSPathsNOn 𝐺 ) 𝑑 ) ) → ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) )
6 5 simpld ⊢ ( ( 𝑡 ∈ ( 𝑎 ( 2 WSPathsNOn 𝐺 ) 𝑏 ) ∧ 𝑡 ∈ ( 𝑐 ( 2 WSPathsNOn 𝐺 ) 𝑑 ) ) → 𝑎 = 𝑐 )
7 6 3adant1 ⊢ ( ( ⊤ ∧ 𝑡 ∈ ( 𝑎 ( 2 WSPathsNOn 𝐺 ) 𝑏 ) ∧ 𝑡 ∈ ( 𝑐 ( 2 WSPathsNOn 𝐺 ) 𝑑 ) ) → 𝑎 = 𝑐 )
8 1 2 4 7 disjiund ⊢ ( ⊤ → Disj 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ( 𝑎 ( 2 WSPathsNOn 𝐺 ) 𝑏 ) )
9 8 mptru ⊢ Disj 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ( 𝑎 ( 2 WSPathsNOn 𝐺 ) 𝑏 )