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	$⊢ \underset{a \in V}{Disj} ⋃_{b \in V ∖ \{a\}} (a (2 WSPathsNOn G) b)$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ a = c \to a (2 WSPathsNOn G) b = c (2 WSPathsNOn G) b$
2		oveq2	$⊢ b = d \to c (2 WSPathsNOn G) b = c (2 WSPathsNOn G) d$
3		sneq	$⊢ a = c \to \{a\} = \{c\}$
4	3	difeq2d	$⊢ a = c \to V ∖ \{a\} = V ∖ \{c\}$
5		wspthneq1eq2	$⊢ (t \in (a (2 WSPathsNOn G) b) \land t \in (c (2 WSPathsNOn G) d)) \to (a = c \land b = d)$
6	5	simpld	$⊢ (t \in (a (2 WSPathsNOn G) b) \land t \in (c (2 WSPathsNOn G) d)) \to a = c$
7	6	3adant1	$⊢ (⊤ \land t \in (a (2 WSPathsNOn G) b) \land t \in (c (2 WSPathsNOn G) d)) \to a = c$
8	1 2 4 7	disjiund	$⊢ ⊤ \to \underset{a \in V}{Disj} ⋃_{b \in V ∖ \{a\}} (a (2 WSPathsNOn G) b)$
9	8	mptru	$⊢ \underset{a \in V}{Disj} ⋃_{b \in V ∖ \{a\}} (a (2 WSPathsNOn G) b)$