Theorem frgr2wwlkeu

Description: For two different vertices in a friendship graph, there is exactly one third vertex being the middle vertex of a (simple) path/walk of length 2 between the two vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 12-May-2021) (Proof shortened by AV, 4-Jan-2022)

	Ref	Expression
Hypothesis	frgr2wwlkeu.v	|- V = ( Vtx ` G )
Assertion	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 ) )

Proof

Step	Hyp	Ref	Expression
1		frgr2wwlkeu.v	|- V = ( Vtx ` G )
2		df-3an	|- ( ( A e. V /\ B e. V /\ A =/= B ) <-> ( ( A e. V /\ B e. V ) /\ A =/= B ) )
3		eqid	|- ( Edg ` G ) = ( Edg ` G )
4	1 3	frcond2	|- ( G e. FriendGraph -> ( ( A e. V /\ B e. V /\ A =/= B ) -> E! c e. V ( { A , c } e. ( Edg ` G ) /\ { c , B } e. ( Edg ` G ) ) ) )
5	2 4	biimtrrid	|- ( G e. FriendGraph -> ( ( ( A e. V /\ B e. V ) /\ A =/= B ) -> E! c e. V ( { A , c } e. ( Edg ` G ) /\ { c , B } e. ( Edg ` G ) ) ) )
6	5	3impib	|- ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> E! c e. V ( { A , c } e. ( Edg ` G ) /\ { c , B } e. ( Edg ` G ) ) )
7		frgrusgr	|- ( G e. FriendGraph -> G e. USGraph )
8		usgrumgr	|- ( G e. USGraph -> G e. UMGraph )
9		3anan32	|- ( ( A e. V /\ c e. V /\ B e. V ) <-> ( ( A e. V /\ B e. V ) /\ c e. V ) )
10	1 3	umgrwwlks2on	|- ( ( G e. UMGraph /\ ( A e. V /\ c e. V /\ B e. V ) ) -> ( <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) <-> ( { A , c } e. ( Edg ` G ) /\ { c , B } e. ( Edg ` G ) ) ) )
11	10	ex	|- ( G e. UMGraph -> ( ( A e. V /\ c e. V /\ B e. V ) -> ( <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) <-> ( { A , c } e. ( Edg ` G ) /\ { c , B } e. ( Edg ` G ) ) ) ) )
12	9 11	biimtrrid	|- ( G e. UMGraph -> ( ( ( A e. V /\ B e. V ) /\ c e. V ) -> ( <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) <-> ( { A , c } e. ( Edg ` G ) /\ { c , B } e. ( Edg ` G ) ) ) ) )
13	7 8 12	3syl	|- ( G e. FriendGraph -> ( ( ( A e. V /\ B e. V ) /\ c e. V ) -> ( <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) <-> ( { A , c } e. ( Edg ` G ) /\ { c , B } e. ( Edg ` G ) ) ) ) )
14	13	impl	|- ( ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) ) /\ c e. V ) -> ( <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) <-> ( { A , c } e. ( Edg ` G ) /\ { c , B } e. ( Edg ` G ) ) ) )
15	14	reubidva	|- ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) ) -> ( E! c e. V <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) <-> E! c e. V ( { A , c } e. ( Edg ` G ) /\ { c , B } e. ( Edg ` G ) ) ) )
16	15	3adant3	|- ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( E! c e. V <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) <-> E! c e. V ( { A , c } e. ( Edg ` G ) /\ { c , B } e. ( Edg ` G ) ) ) )
17	6 16	mpbird	|- ( ( G e. FriendGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> E! c e. V <" A c B "> e. ( A ( 2 WWalksNOn G ) B ) )