Metamath Proof Explorer

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∈V|D⁡x=K
frgrwopreg.b ⊢B=V∖A
frgrwopreg.e ⊢E=Edg⁡G
Assertion frgrwopregasn ⊢G∈FriendGraph∧X∈V∧A=X→∀w∈V∖XXw∈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→∀v∈A∀w∈Bvw∈E
7 snidg ⊢X∈V→X∈X
8 7 adantr ⊢X∈V∧A=X→X∈X
9 eleq2 ⊢A=X→X∈A↔X∈X
10 9 adantl ⊢X∈V∧A=X→X∈A↔X∈X
11 8 10 mpbird ⊢X∈V∧A=X→X∈A
12 preq1 ⊢v=X→vw=Xw
13 12 eleq1d ⊢v=X→vw∈E↔Xw∈E
14 13 ralbidv ⊢v=X→∀w∈Bvw∈E↔∀w∈BXw∈E
15 14 rspcv ⊢X∈A→∀v∈A∀w∈Bvw∈E→∀w∈BXw∈E
16 11 15 syl ⊢X∈V∧A=X→∀v∈A∀w∈Bvw∈E→∀w∈BXw∈E
17 difeq2 ⊢A=X→V∖A=V∖X
18 4 17 eqtrid ⊢A=X→B=V∖X
19 18 adantl ⊢X∈V∧A=X→B=V∖X
20 19 raleqdv ⊢X∈V∧A=X→∀w∈BXw∈E↔∀w∈V∖XXw∈E
21 16 20 sylibd ⊢X∈V∧A=X→∀v∈A∀w∈Bvw∈E→∀w∈V∖XXw∈E
22 6 21 syl5com ⊢G∈FriendGraph→X∈V∧A=X→∀w∈V∖XXw∈E
23 22 3impib ⊢G∈FriendGraph∧X∈V∧A=X→∀w∈V∖XXw∈E