Metamath Proof Explorer

Theorem frgr2wwlkn0

Description: In a friendship graph, there is always a path/walk of length 2 between two different vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 12-May-2021)

		Ref	Expression
	Hypothesis	frgr2wwlkeu.v	$⊢ V = Vtx (G)$
	Assertion	frgr2wwlkn0	$⊢ (G \in FriendGraph \land (A \in V \land B \in V) \land A \neq B) \to A (2 WWalksNOn G) B \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		frgr2wwlkeu.v	$⊢ V = Vtx (G)$
2	1	frgr2wwlkeu	$⊢ (G \in FriendGraph \land (A \in V \land B \in V) \land A \neq B) \to \exists! c \in V ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)$
3		reurex	$⊢ \exists! c \in V ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B) \to \exists c \in V ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)$
4		ne0i	$⊢ ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B) \to A (2 WWalksNOn G) B \neq \emptyset$
5	4	rexlimivw	$⊢ \exists c \in V ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B) \to A (2 WWalksNOn G) B \neq \emptyset$
6	2 3 5	3syl	$⊢ (G \in FriendGraph \land (A \in V \land B \in V) \land A \neq B) \to A (2 WWalksNOn G) B \neq \emptyset$