Theorem frgrwopregbsn

Description: According to statement 5 in Huneke p. 2: "If ... B is a singleton, then that singleton is a universal friend". This version of frgrwopreg2 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 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	frgrwopregbsn	|- ( ( G e. FriendGraph /\ X e. V /\ B = { 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. w e. A A. v e. B { w , v } e. E )
7		ralcom	|- ( A. w e. A A. v e. B { w , v } e. E <-> A. v e. B A. w e. A { w , v } e. E )
8		snidg	|- ( X e. V -> X e. { X } )
9	8	adantr	|- ( ( X e. V /\ B = { X } ) -> X e. { X } )
10		eleq2	|- ( B = { X } -> ( X e. B <-> X e. { X } ) )
11	10	adantl	|- ( ( X e. V /\ B = { X } ) -> ( X e. B <-> X e. { X } ) )
12	9 11	mpbird	|- ( ( X e. V /\ B = { X } ) -> X e. B )
13		preq2	|- ( v = X -> { w , v } = { w , X } )
14		prcom	|- { w , X } = { X , w }
15	13 14	eqtrdi	|- ( v = X -> { w , v } = { X , w } )
16	15	eleq1d	|- ( v = X -> ( { w , v } e. E <-> { X , w } e. E ) )
17	16	ralbidv	|- ( v = X -> ( A. w e. A { w , v } e. E <-> A. w e. A { X , w } e. E ) )
18	17	rspcv	|- ( X e. B -> ( A. v e. B A. w e. A { w , v } e. E -> A. w e. A { X , w } e. E ) )
19	12 18	syl	|- ( ( X e. V /\ B = { X } ) -> ( A. v e. B A. w e. A { w , v } e. E -> A. w e. A { X , w } e. E ) )
20	3	ssrab3	|- A C_ V
21		ssdifim	|- ( ( A C_ V /\ B = ( V \ A ) ) -> A = ( V \ B ) )
22	20 4 21	mp2an	|- A = ( V \ B )
23		difeq2	|- ( B = { X } -> ( V \ B ) = ( V \ { X } ) )
24	23	adantl	|- ( ( X e. V /\ B = { X } ) -> ( V \ B ) = ( V \ { X } ) )
25	22 24	syl5eq	|- ( ( X e. V /\ B = { X } ) -> A = ( V \ { X } ) )
26	25	raleqdv	|- ( ( X e. V /\ B = { X } ) -> ( A. w e. A { X , w } e. E <-> A. w e. ( V \ { X } ) { X , w } e. E ) )
27	19 26	sylibd	|- ( ( X e. V /\ B = { X } ) -> ( A. v e. B A. w e. A { w , v } e. E -> A. w e. ( V \ { X } ) { X , w } e. E ) )
28	7 27	syl5bi	|- ( ( X e. V /\ B = { X } ) -> ( A. w e. A A. v e. B { w , v } e. E -> A. w e. ( V \ { X } ) { X , w } e. E ) )
29	6 28	syl5com	|- ( G e. FriendGraph -> ( ( X e. V /\ B = { X } ) -> A. w e. ( V \ { X } ) { X , w } e. E ) )
30	29	3impib	|- ( ( G e. FriendGraph /\ X e. V /\ B = { X } ) -> A. w e. ( V \ { X } ) { X , w } e. E )