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 e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( A ( 2 WWalksNOn G ) B ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		frgr2wwlkeu.v	|- V = ( Vtx ` G )
2	1	frgr2wwlkeu	|- ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> E! c e. V <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) )
3		reurex	|- ( E! c e. V <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) -> E. c e. V <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) )
4		ne0i	|- ( <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) -> ( A ( 2 WWalksNOn G ) B ) =/= (/) )
5	4	rexlimivw	|- ( E. c e. V <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) -> ( A ( 2 WWalksNOn G ) B ) =/= (/) )
6	2 3 5	3syl	|- ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( A ( 2 WWalksNOn G ) B ) =/= (/) )