Metamath Proof Explorer

Theorem 2wspdisj

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

		Ref	Expression
	Assertion	2wspdisj	$⊢ \underset{b \in V ∖ \{A\}}{Disj} (A (2 WSPathsNOn G) b)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ b = c \to A (2 WSPathsNOn G) b = A (2 WSPathsNOn G) c$
2		wspthneq1eq2	$⊢ (t \in (A (2 WSPathsNOn G) b) \land t \in (A (2 WSPathsNOn G) c)) \to (A = A \land b = c)$
3	2	simprd	$⊢ (t \in (A (2 WSPathsNOn G) b) \land t \in (A (2 WSPathsNOn G) c)) \to b = c$
4	3	3adant1	$⊢ (⊤ \land t \in (A (2 WSPathsNOn G) b) \land t \in (A (2 WSPathsNOn G) c)) \to b = c$
5	1 4	disjord	$⊢ ⊤ \to \underset{b \in V ∖ \{A\}}{Disj} (A (2 WSPathsNOn G) b)$
6	5	mptru	$⊢ \underset{b \in V ∖ \{A\}}{Disj} (A (2 WSPathsNOn G) b)$