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)\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\forall v\in B\left\{w,v\right\}\in E$$
7		ralcom	$$⊢\forall w\in A\forall v\in B\left\{w,v\right\}\in E\leftrightarrow \forall v\in B\forall w\in A\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\leftrightarrow X\in \left\{X\right\}\right)$$
11	10	adantl	$$⊢\left(X\in V\wedge B=\left\{X\right\}\right)\to \left(X\in B\leftrightarrow 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	eqtrdi	$$⊢v=X\to \left\{w,v\right\}=\left\{X,w\right\}$$
16	15	eleq1d	$$⊢v=X\to \left(\left\{w,v\right\}\in E\leftrightarrow \left\{X,w\right\}\in E\right)$$
17	16	ralbidv	$$⊢v=X\to \left(\forall w\in A\left\{w,v\right\}\in E\leftrightarrow \forall w\in A\left\{X,w\right\}\in E\right)$$
18	17	rspcv	$$⊢X\in B\to \left(\forall v\in B\forall w\in A\left\{w,v\right\}\in E\to \forall w\in A\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\forall w\in A\left\{w,v\right\}\in E\to \forall w\in A\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	eqtrid	$$⊢\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\left\{X,w\right\}\in E\leftrightarrow \forall w\in \left(V\setminus \left\{X\right\}\right)\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\forall w\in A\left\{w,v\right\}\in E\to \forall w\in \left(V\setminus \left\{X\right\}\right)\left\{X,w\right\}\in E\right)$$
28	7 27	biimtrid	$$⊢\left(X\in V\wedge B=\left\{X\right\}\right)\to \left(\forall w\in A\forall v\in B\left\{w,v\right\}\in E\to \forall w\in \left(V\setminus \left\{X\right\}\right)\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)\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)\left\{X,w\right\}\in E$$