Theorem frgrwopregasn

Description: According to statement 5 in Huneke p. 2: "If A ... is a singleton, then that singleton is a universal friend". This version of frgrwopreg1 is stricter (claiming that the singleton itself is a universal friend instead of claiming the existence of a universal friend only) and therefore closer to Huneke's statement. This strict variant, however, is not required for the proof of the friendship theorem. (Contributed by Alexander van der Vekens, 1-Jan-2018) (Revised by AV, 4-Feb-2022)

	Ref	Expression
Hypotheses	frgrwopreg.v	|- V = ( Vtx ` G )
	frgrwopreg.d	|- D = ( VtxDeg ` G )
	frgrwopreg.a	|- A = { x e. V | ( D ` x ) = K }
	frgrwopreg.b	|- B = ( V \ A )
	frgrwopreg.e	|- E = ( Edg ` G )
Assertion	frgrwopregasn	|- ( ( G e. FriendGraph /\ X e. V /\ A = { X } ) -> A. w e. ( V \ { X } ) { X , w } e. E )

Proof

Step	Hyp	Ref	Expression
1		frgrwopreg.v	|- V = ( Vtx ` G )
2		frgrwopreg.d	|- D = ( VtxDeg ` G )
3		frgrwopreg.a	|- A = { x e. V | ( D ` x ) = K }
4		frgrwopreg.b	|- B = ( V \ A )
5		frgrwopreg.e	|- E = ( Edg ` G )
6	1 2 3 4 5	frgrwopreglem4	|- ( G e. FriendGraph -> A. v e. A A. w e. B { v , w } e. E )
7		snidg	|- ( X e. V -> X e. { X } )
8	7	adantr	|- ( ( X e. V /\ A = { X } ) -> X e. { X } )
9		eleq2	|- ( A = { X } -> ( X e. A <-> X e. { X } ) )
10	9	adantl	|- ( ( X e. V /\ A = { X } ) -> ( X e. A <-> X e. { X } ) )
11	8 10	mpbird	|- ( ( X e. V /\ A = { X } ) -> X e. A )
12		preq1	|- ( v = X -> { v , w } = { X , w } )
13	12	eleq1d	|- ( v = X -> ( { v , w } e. E <-> { X , w } e. E ) )
14	13	ralbidv	|- ( v = X -> ( A. w e. B { v , w } e. E <-> A. w e. B { X , w } e. E ) )
15	14	rspcv	|- ( X e. A -> ( A. v e. A A. w e. B { v , w } e. E -> A. w e. B { X , w } e. E ) )
16	11 15	syl	|- ( ( X e. V /\ A = { X } ) -> ( A. v e. A A. w e. B { v , w } e. E -> A. w e. B { X , w } e. E ) )
17		difeq2	|- ( A = { X } -> ( V \ A ) = ( V \ { X } ) )
18	4 17	syl5eq	|- ( A = { X } -> B = ( V \ { X } ) )
19	18	adantl	|- ( ( X e. V /\ A = { X } ) -> B = ( V \ { X } ) )
20	19	raleqdv	|- ( ( X e. V /\ A = { X } ) -> ( A. w e. B { X , w } e. E <-> A. w e. ( V \ { X } ) { X , w } e. E ) )
21	16 20	sylibd	|- ( ( X e. V /\ A = { X } ) -> ( A. v e. A A. w e. B { v , w } e. E -> A. w e. ( V \ { X } ) { X , w } e. E ) )
22	6 21	syl5com	|- ( G e. FriendGraph -> ( ( X e. V /\ A = { X } ) -> A. w e. ( V \ { X } ) { X , w } e. E ) )
23	22	3impib	|- ( ( G e. FriendGraph /\ X e. V /\ A = { X } ) -> A. w e. ( V \ { X } ) { X , w } e. E )