# 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}=\mathrm{Vtx}\left({G}\right)$
frgrwopreg.d ${⊢}{D}=\mathrm{VtxDeg}\left({G}\right)$
frgrwopreg.a ${⊢}{A}=\left\{{x}\in {V}|{D}\left({x}\right)={K}\right\}$
frgrwopreg.b ${⊢}{B}={V}\setminus {A}$
frgrwopreg.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion frgrwopregbsn ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge {X}\in {V}\wedge {B}=\left\{{X}\right\}\right)\to \forall {w}\in \left({V}\setminus \left\{{X}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{X},{w}\right\}\in {E}$

### Proof

Step Hyp Ref Expression
1 frgrwopreg.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 frgrwopreg.d ${⊢}{D}=\mathrm{VtxDeg}\left({G}\right)$
3 frgrwopreg.a ${⊢}{A}=\left\{{x}\in {V}|{D}\left({x}\right)={K}\right\}$
4 frgrwopreg.b ${⊢}{B}={V}\setminus {A}$
5 frgrwopreg.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
6 1 2 3 4 5 frgrwopreglem4 ${⊢}{G}\in \mathrm{FriendGraph}\to \forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{w},{v}\right\}\in {E}$
7 ralcom ${⊢}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{w},{v}\right\}\in {E}↔\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left\{{w},{v}\right\}\in {E}$
8 snidg ${⊢}{X}\in {V}\to {X}\in \left\{{X}\right\}$
9 8 adantr ${⊢}\left({X}\in {V}\wedge {B}=\left\{{X}\right\}\right)\to {X}\in \left\{{X}\right\}$
10 eleq2 ${⊢}{B}=\left\{{X}\right\}\to \left({X}\in {B}↔{X}\in \left\{{X}\right\}\right)$
11 10 adantl ${⊢}\left({X}\in {V}\wedge {B}=\left\{{X}\right\}\right)\to \left({X}\in {B}↔{X}\in \left\{{X}\right\}\right)$
12 9 11 mpbird ${⊢}\left({X}\in {V}\wedge {B}=\left\{{X}\right\}\right)\to {X}\in {B}$
13 preq2 ${⊢}{v}={X}\to \left\{{w},{v}\right\}=\left\{{w},{X}\right\}$
14 prcom ${⊢}\left\{{w},{X}\right\}=\left\{{X},{w}\right\}$
15 13 14 syl6eq ${⊢}{v}={X}\to \left\{{w},{v}\right\}=\left\{{X},{w}\right\}$
16 15 eleq1d ${⊢}{v}={X}\to \left(\left\{{w},{v}\right\}\in {E}↔\left\{{X},{w}\right\}\in {E}\right)$
17 16 ralbidv ${⊢}{v}={X}\to \left(\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left\{{w},{v}\right\}\in {E}↔\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left\{{X},{w}\right\}\in {E}\right)$
18 17 rspcv ${⊢}{X}\in {B}\to \left(\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left\{{w},{v}\right\}\in {E}\to \forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left\{{X},{w}\right\}\in {E}\right)$
19 12 18 syl ${⊢}\left({X}\in {V}\wedge {B}=\left\{{X}\right\}\right)\to \left(\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left\{{w},{v}\right\}\in {E}\to \forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left\{{X},{w}\right\}\in {E}\right)$
20 3 ssrab3 ${⊢}{A}\subseteq {V}$
21 ssdifim ${⊢}\left({A}\subseteq {V}\wedge {B}={V}\setminus {A}\right)\to {A}={V}\setminus {B}$
22 20 4 21 mp2an ${⊢}{A}={V}\setminus {B}$
23 difeq2 ${⊢}{B}=\left\{{X}\right\}\to {V}\setminus {B}={V}\setminus \left\{{X}\right\}$
24 23 adantl ${⊢}\left({X}\in {V}\wedge {B}=\left\{{X}\right\}\right)\to {V}\setminus {B}={V}\setminus \left\{{X}\right\}$
25 22 24 syl5eq ${⊢}\left({X}\in {V}\wedge {B}=\left\{{X}\right\}\right)\to {A}={V}\setminus \left\{{X}\right\}$
26 25 raleqdv ${⊢}\left({X}\in {V}\wedge {B}=\left\{{X}\right\}\right)\to \left(\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left\{{X},{w}\right\}\in {E}↔\forall {w}\in \left({V}\setminus \left\{{X}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{X},{w}\right\}\in {E}\right)$
27 19 26 sylibd ${⊢}\left({X}\in {V}\wedge {B}=\left\{{X}\right\}\right)\to \left(\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left\{{w},{v}\right\}\in {E}\to \forall {w}\in \left({V}\setminus \left\{{X}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{X},{w}\right\}\in {E}\right)$
28 7 27 syl5bi ${⊢}\left({X}\in {V}\wedge {B}=\left\{{X}\right\}\right)\to \left(\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\left\{{w},{v}\right\}\in {E}\to \forall {w}\in \left({V}\setminus \left\{{X}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{X},{w}\right\}\in {E}\right)$
29 6 28 syl5com ${⊢}{G}\in \mathrm{FriendGraph}\to \left(\left({X}\in {V}\wedge {B}=\left\{{X}\right\}\right)\to \forall {w}\in \left({V}\setminus \left\{{X}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{X},{w}\right\}\in {E}\right)$
30 29 3impib ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge {X}\in {V}\wedge {B}=\left\{{X}\right\}\right)\to \forall {w}\in \left({V}\setminus \left\{{X}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{X},{w}\right\}\in {E}$