Theorem frgreu

Description: Variant of frcond2 : Any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 12-May-2021) (Proof shortened by AV, 4-Jan-2022)

	Ref	Expression
Hypotheses	frcond1.v	|- V = ( Vtx ` G )
	frcond1.e	|- E = ( Edg ` G )
Assertion	frgreu	|- ( G e. FriendGraph -> ( ( A e. V /\ C e. V /\ A =/= C ) -> E! b ( { A , b } e. E /\ { b , C } e. E ) ) )

Proof

Step	Hyp	Ref	Expression
1		frcond1.v	|- V = ( Vtx ` G )
2		frcond1.e	|- E = ( Edg ` G )
3	1 2	frcond2	|- ( G e. FriendGraph -> ( ( A e. V /\ C e. V /\ A =/= C ) -> E! b e. V ( { A , b } e. E /\ { b , C } e. E ) ) )
4	3	imp	|- ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) -> E! b e. V ( { A , b } e. E /\ { b , C } e. E ) )
5		frgrusgr	|- ( G e. FriendGraph -> G e. USGraph )
6	5	adantr	|- ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) -> G e. USGraph )
7		simpl	|- ( ( { A , b } e. E /\ { b , C } e. E ) -> { A , b } e. E )
8	2 1	usgrpredgv	|- ( ( G e. USGraph /\ { A , b } e. E ) -> ( A e. V /\ b e. V ) )
9	8	simprd	|- ( ( G e. USGraph /\ { A , b } e. E ) -> b e. V )
10	6 7 9	syl2an	|- ( ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) /\ ( { A , b } e. E /\ { b , C } e. E ) ) -> b e. V )
11	10	reueubd	|- ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) -> ( E! b e. V ( { A , b } e. E /\ { b , C } e. E ) <-> E! b ( { A , b } e. E /\ { b , C } e. E ) ) )
12	4 11	mpbid	|- ( ( G e. FriendGraph /\ ( A e. V /\ C e. V /\ A =/= C ) ) -> E! b ( { A , b } e. E /\ { b , C } e. E ) )
13	12	ex	|- ( G e. FriendGraph -> ( ( A e. V /\ C e. V /\ A =/= C ) -> E! b ( { A , b } e. E /\ { b , C } e. E ) ) )