Theorem 1to3vfriendship

Description: The friendship theorem for small graphs: In every friendship graph with one, two or three vertices, there is a vertex which is adjacent to all other vertices. (Contributed by Alexander van der Vekens, 6-Oct-2017) (Revised by AV, 31-Mar-2021)

	Ref	Expression
Hypotheses	3vfriswmgr.v	|- V = ( Vtx ` G )
	3vfriswmgr.e	|- E = ( Edg ` G )
Assertion	1to3vfriendship	|- ( ( A e. X /\ ( V = { A } \/ V = { A , B } \/ V = { A , B , C } ) ) -> ( G e. FriendGraph -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )

Proof

Step	Hyp	Ref	Expression
1		3vfriswmgr.v	|- V = ( Vtx ` G )
2		3vfriswmgr.e	|- E = ( Edg ` G )
3	1 2	1to3vfriswmgr	|- ( ( A e. X /\ ( V = { A } \/ V = { A , B } \/ V = { A , B , C } ) ) -> ( G e. FriendGraph -> E. v e. V A. w e. ( V \ { v } ) ( { w , v } e. E /\ E! x e. ( V \ { v } ) { w , x } e. E ) ) )
4		prcom	|- { w , v } = { v , w }
5	4	eleq1i	|- ( { w , v } e. E <-> { v , w } e. E )
6	5	biimpi	|- ( { w , v } e. E -> { v , w } e. E )
7	6	adantr	|- ( ( { w , v } e. E /\ E! x e. ( V \ { v } ) { w , x } e. E ) -> { v , w } e. E )
8	7	ralimi	|- ( A. w e. ( V \ { v } ) ( { w , v } e. E /\ E! x e. ( V \ { v } ) { w , x } e. E ) -> A. w e. ( V \ { v } ) { v , w } e. E )
9	8	reximi	|- ( E. v e. V A. w e. ( V \ { v } ) ( { w , v } e. E /\ E! x e. ( V \ { v } ) { w , x } e. E ) -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E )
10	3 9	syl6	|- ( ( A e. X /\ ( V = { A } \/ V = { A , B } \/ V = { A , B , C } ) ) -> ( G e. FriendGraph -> E. v e. V A. w e. ( V \ { v } ) { v , w } e. E ) )