# Metamath Proof Explorer

## Theorem frcond4

Description: The friendship condition, alternatively expressed by neighborhoods: in a friendship graph, the neighborhoods of two different vertices have exactly one vertex in common. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 29-Mar-2021) (Proof shortened by AV, 30-Dec-2021)

Ref Expression
Hypotheses frcond1.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
frcond1.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion frcond4 ${⊢}{G}\in \mathrm{FriendGraph}\to \forall {k}\in {V}\phantom{\rule{.4em}{0ex}}\forall {l}\in \left({V}\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({G}\mathrm{NeighbVtx}{k}\right)\cap \left({G}\mathrm{NeighbVtx}{l}\right)=\left\{{x}\right\}$

### Proof

Step Hyp Ref Expression
1 frcond1.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 frcond1.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 1 2 frcond3 ${⊢}{G}\in \mathrm{FriendGraph}\to \left(\left({k}\in {V}\wedge {l}\in {V}\wedge {k}\ne {l}\right)\to \exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({G}\mathrm{NeighbVtx}{k}\right)\cap \left({G}\mathrm{NeighbVtx}{l}\right)=\left\{{x}\right\}\right)$
4 eldifsn ${⊢}{l}\in \left({V}\setminus \left\{{k}\right\}\right)↔\left({l}\in {V}\wedge {l}\ne {k}\right)$
5 necom ${⊢}{l}\ne {k}↔{k}\ne {l}$
6 5 biimpi ${⊢}{l}\ne {k}\to {k}\ne {l}$
7 6 anim2i ${⊢}\left({l}\in {V}\wedge {l}\ne {k}\right)\to \left({l}\in {V}\wedge {k}\ne {l}\right)$
8 4 7 sylbi ${⊢}{l}\in \left({V}\setminus \left\{{k}\right\}\right)\to \left({l}\in {V}\wedge {k}\ne {l}\right)$
9 8 anim2i ${⊢}\left({k}\in {V}\wedge {l}\in \left({V}\setminus \left\{{k}\right\}\right)\right)\to \left({k}\in {V}\wedge \left({l}\in {V}\wedge {k}\ne {l}\right)\right)$
10 3anass ${⊢}\left({k}\in {V}\wedge {l}\in {V}\wedge {k}\ne {l}\right)↔\left({k}\in {V}\wedge \left({l}\in {V}\wedge {k}\ne {l}\right)\right)$
11 9 10 sylibr ${⊢}\left({k}\in {V}\wedge {l}\in \left({V}\setminus \left\{{k}\right\}\right)\right)\to \left({k}\in {V}\wedge {l}\in {V}\wedge {k}\ne {l}\right)$
12 3 11 impel ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge \left({k}\in {V}\wedge {l}\in \left({V}\setminus \left\{{k}\right\}\right)\right)\right)\to \exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({G}\mathrm{NeighbVtx}{k}\right)\cap \left({G}\mathrm{NeighbVtx}{l}\right)=\left\{{x}\right\}$
13 12 ralrimivva ${⊢}{G}\in \mathrm{FriendGraph}\to \forall {k}\in {V}\phantom{\rule{.4em}{0ex}}\forall {l}\in \left({V}\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({G}\mathrm{NeighbVtx}{k}\right)\cap \left({G}\mathrm{NeighbVtx}{l}\right)=\left\{{x}\right\}$