Metamath Proof Explorer

Theorem frcond1

Description: The friendship condition: any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 29-Mar-2021)

Ref Expression
Hypotheses frcond1.v ⊢V=Vtx⁡G
frcond1.e ⊢E=Edg⁡G
Assertion frcond1 ⊢G∈FriendGraph→A∈V∧C∈V∧A≠C→∃!b∈VAbbC⊆E

Proof

Step Hyp Ref Expression
1 frcond1.v ⊢V=Vtx⁡G
2 frcond1.e ⊢E=Edg⁡G
3 1 2 isfrgr ⊢G∈FriendGraph↔G∈USGraph∧∀k∈V∀l∈V∖k∃!b∈Vbkbl⊆E
4 preq2 ⊢k=A→bk=bA
5 4 preq1d ⊢k=A→bkbl=bAbl
6 5 sseq1d ⊢k=A→bkbl⊆E↔bAbl⊆E
7 6 reubidv ⊢k=A→∃!b∈Vbkbl⊆E↔∃!b∈VbAbl⊆E
8 preq2 ⊢l=C→bl=bC
9 8 preq2d ⊢l=C→bAbl=bAbC
10 9 sseq1d ⊢l=C→bAbl⊆E↔bAbC⊆E
11 10 reubidv ⊢l=C→∃!b∈VbAbl⊆E↔∃!b∈VbAbC⊆E
12 simp1 ⊢A∈V∧C∈V∧A≠C→A∈V
13 sneq ⊢k=A→k=A
14 13 difeq2d ⊢k=A→V∖k=V∖A
15 14 adantl ⊢A∈V∧C∈V∧A≠C∧k=A→V∖k=V∖A
16 necom ⊢A≠C↔C≠A
17 16 biimpi ⊢A≠C→C≠A
18 17 anim2i ⊢C∈V∧A≠C→C∈V∧C≠A
19 18 3adant1 ⊢A∈V∧C∈V∧A≠C→C∈V∧C≠A
20 eldifsn ⊢C∈V∖A↔C∈V∧C≠A
21 19 20 sylibr ⊢A∈V∧C∈V∧A≠C→C∈V∖A
22 7 11 12 15 21 rspc2vd ⊢A∈V∧C∈V∧A≠C→∀k∈V∀l∈V∖k∃!b∈Vbkbl⊆E→∃!b∈VbAbC⊆E
23 prcom ⊢bA=Ab
24 23 preq1i ⊢bAbC=AbbC
25 24 sseq1i ⊢bAbC⊆E↔AbbC⊆E
26 25 reubii ⊢∃!b∈VbAbC⊆E↔∃!b∈VAbbC⊆E
27 26 biimpi ⊢∃!b∈VbAbC⊆E→∃!b∈VAbbC⊆E
28 22 27 syl6com ⊢∀k∈V∀l∈V∖k∃!b∈Vbkbl⊆E→A∈V∧C∈V∧A≠C→∃!b∈VAbbC⊆E
29 3 28 simplbiim ⊢G∈FriendGraph→A∈V∧C∈V∧A≠C→∃!b∈VAbbC⊆E