Metamath Proof Explorer


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 V | D x = K
frgrwopreg.b B = V A
frgrwopreg.e E = Edg G
Assertion frgrwopregbsn G FriendGraph X V B = X w V X X w E

Proof

Step Hyp Ref Expression
1 frgrwopreg.v V = Vtx G
2 frgrwopreg.d D = VtxDeg G
3 frgrwopreg.a A = x V | D x = K
4 frgrwopreg.b B = V A
5 frgrwopreg.e E = Edg G
6 1 2 3 4 5 frgrwopreglem4 G FriendGraph w A v B w v E
7 ralcom w A v B w v E v B w A w v E
8 snidg X V X X
9 8 adantr X V B = X X X
10 eleq2 B = X X B X X
11 10 adantl X V B = X X B X X
12 9 11 mpbird X V B = X X B
13 preq2 v = X w v = w X
14 prcom w X = X w
15 13 14 syl6eq v = X w v = X w
16 15 eleq1d v = X w v E X w E
17 16 ralbidv v = X w A w v E w A X w E
18 17 rspcv X B v B w A w v E w A X w E
19 12 18 syl X V B = X v B w A w v E w A X w E
20 3 ssrab3 A V
21 ssdifim A 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 V B = X V B = V X
25 22 24 syl5eq X V B = X A = V X
26 25 raleqdv X V B = X w A X w E w V X X w E
27 19 26 sylibd X V B = X v B w A w v E w V X X w E
28 7 27 syl5bi X V B = X w A v B w v E w V X X w E
29 6 28 syl5com G FriendGraph X V B = X w V X X w E
30 29 3impib G FriendGraph X V B = X w V X X w E