# Metamath Proof Explorer

## Theorem frcond3

Description: The friendship condition, expressed by neighborhoods: in a friendship graph, the neighborhood of a vertex and the neighborhood of a second, different vertex have exactly one vertex in common. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised 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 frcond3 ${⊢}{G}\in \mathrm{FriendGraph}\to \left(\left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\to \exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({G}\mathrm{NeighbVtx}{A}\right)\cap \left({G}\mathrm{NeighbVtx}{C}\right)=\left\{{x}\right\}\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 frcond1 ${⊢}{G}\in \mathrm{FriendGraph}\to \left(\left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\to \exists !{b}\in {V}\phantom{\rule{.4em}{0ex}}\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right)$
4 3 imp ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\right)\to \exists !{b}\in {V}\phantom{\rule{.4em}{0ex}}\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}$
5 ssrab2 ${⊢}\left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}\subseteq {V}$
6 sseq1 ${⊢}\left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}=\left\{{x}\right\}\to \left(\left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}\subseteq {V}↔\left\{{x}\right\}\subseteq {V}\right)$
7 5 6 mpbii ${⊢}\left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}=\left\{{x}\right\}\to \left\{{x}\right\}\subseteq {V}$
8 vex ${⊢}{x}\in \mathrm{V}$
9 8 snss ${⊢}{x}\in {V}↔\left\{{x}\right\}\subseteq {V}$
10 7 9 sylibr ${⊢}\left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}=\left\{{x}\right\}\to {x}\in {V}$
11 10 adantl ${⊢}\left(\left({G}\in \mathrm{FriendGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\right)\wedge \left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}=\left\{{x}\right\}\right)\to {x}\in {V}$
12 frgrusgr ${⊢}{G}\in \mathrm{FriendGraph}\to {G}\in \mathrm{USGraph}$
13 1 2 nbusgr ${⊢}{G}\in \mathrm{USGraph}\to {G}\mathrm{NeighbVtx}{A}=\left\{{b}\in {V}|\left\{{A},{b}\right\}\in {E}\right\}$
14 1 2 nbusgr ${⊢}{G}\in \mathrm{USGraph}\to {G}\mathrm{NeighbVtx}{C}=\left\{{b}\in {V}|\left\{{C},{b}\right\}\in {E}\right\}$
15 13 14 ineq12d ${⊢}{G}\in \mathrm{USGraph}\to \left({G}\mathrm{NeighbVtx}{A}\right)\cap \left({G}\mathrm{NeighbVtx}{C}\right)=\left\{{b}\in {V}|\left\{{A},{b}\right\}\in {E}\right\}\cap \left\{{b}\in {V}|\left\{{C},{b}\right\}\in {E}\right\}$
16 12 15 syl ${⊢}{G}\in \mathrm{FriendGraph}\to \left({G}\mathrm{NeighbVtx}{A}\right)\cap \left({G}\mathrm{NeighbVtx}{C}\right)=\left\{{b}\in {V}|\left\{{A},{b}\right\}\in {E}\right\}\cap \left\{{b}\in {V}|\left\{{C},{b}\right\}\in {E}\right\}$
17 16 adantr ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\right)\to \left({G}\mathrm{NeighbVtx}{A}\right)\cap \left({G}\mathrm{NeighbVtx}{C}\right)=\left\{{b}\in {V}|\left\{{A},{b}\right\}\in {E}\right\}\cap \left\{{b}\in {V}|\left\{{C},{b}\right\}\in {E}\right\}$
18 17 adantr ${⊢}\left(\left({G}\in \mathrm{FriendGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\right)\wedge \left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}=\left\{{x}\right\}\right)\to \left({G}\mathrm{NeighbVtx}{A}\right)\cap \left({G}\mathrm{NeighbVtx}{C}\right)=\left\{{b}\in {V}|\left\{{A},{b}\right\}\in {E}\right\}\cap \left\{{b}\in {V}|\left\{{C},{b}\right\}\in {E}\right\}$
19 inrab ${⊢}\left\{{b}\in {V}|\left\{{A},{b}\right\}\in {E}\right\}\cap \left\{{b}\in {V}|\left\{{C},{b}\right\}\in {E}\right\}=\left\{{b}\in {V}|\left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{C},{b}\right\}\in {E}\right)\right\}$
20 18 19 syl6eq ${⊢}\left(\left({G}\in \mathrm{FriendGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\right)\wedge \left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}=\left\{{x}\right\}\right)\to \left({G}\mathrm{NeighbVtx}{A}\right)\cap \left({G}\mathrm{NeighbVtx}{C}\right)=\left\{{b}\in {V}|\left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{C},{b}\right\}\in {E}\right)\right\}$
21 prcom ${⊢}\left\{{C},{b}\right\}=\left\{{b},{C}\right\}$
22 21 eleq1i ${⊢}\left\{{C},{b}\right\}\in {E}↔\left\{{b},{C}\right\}\in {E}$
23 22 anbi2i ${⊢}\left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{C},{b}\right\}\in {E}\right)↔\left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)$
24 prex ${⊢}\left\{{A},{b}\right\}\in \mathrm{V}$
25 prex ${⊢}\left\{{b},{C}\right\}\in \mathrm{V}$
26 24 25 prss ${⊢}\left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)↔\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}$
27 23 26 bitri ${⊢}\left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{C},{b}\right\}\in {E}\right)↔\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}$
28 27 a1i ${⊢}\left(\left({G}\in \mathrm{FriendGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\right)\wedge {b}\in {V}\right)\to \left(\left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{C},{b}\right\}\in {E}\right)↔\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right)$
29 28 rabbidva ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\right)\to \left\{{b}\in {V}|\left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{C},{b}\right\}\in {E}\right)\right\}=\left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}$
30 29 adantr ${⊢}\left(\left({G}\in \mathrm{FriendGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\right)\wedge \left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}=\left\{{x}\right\}\right)\to \left\{{b}\in {V}|\left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{C},{b}\right\}\in {E}\right)\right\}=\left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}$
31 simpr ${⊢}\left(\left({G}\in \mathrm{FriendGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\right)\wedge \left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}=\left\{{x}\right\}\right)\to \left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}=\left\{{x}\right\}$
32 20 30 31 3eqtrd ${⊢}\left(\left({G}\in \mathrm{FriendGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\right)\wedge \left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}=\left\{{x}\right\}\right)\to \left({G}\mathrm{NeighbVtx}{A}\right)\cap \left({G}\mathrm{NeighbVtx}{C}\right)=\left\{{x}\right\}$
33 11 32 jca ${⊢}\left(\left({G}\in \mathrm{FriendGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\right)\wedge \left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}=\left\{{x}\right\}\right)\to \left({x}\in {V}\wedge \left({G}\mathrm{NeighbVtx}{A}\right)\cap \left({G}\mathrm{NeighbVtx}{C}\right)=\left\{{x}\right\}\right)$
34 33 ex ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\right)\to \left(\left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}=\left\{{x}\right\}\to \left({x}\in {V}\wedge \left({G}\mathrm{NeighbVtx}{A}\right)\cap \left({G}\mathrm{NeighbVtx}{C}\right)=\left\{{x}\right\}\right)\right)$
35 34 eximdv ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}=\left\{{x}\right\}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {V}\wedge \left({G}\mathrm{NeighbVtx}{A}\right)\cap \left({G}\mathrm{NeighbVtx}{C}\right)=\left\{{x}\right\}\right)\right)$
36 reusn ${⊢}\exists !{b}\in {V}\phantom{\rule{.4em}{0ex}}\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left\{{b}\in {V}|\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\right\}=\left\{{x}\right\}$
37 df-rex ${⊢}\exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({G}\mathrm{NeighbVtx}{A}\right)\cap \left({G}\mathrm{NeighbVtx}{C}\right)=\left\{{x}\right\}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {V}\wedge \left({G}\mathrm{NeighbVtx}{A}\right)\cap \left({G}\mathrm{NeighbVtx}{C}\right)=\left\{{x}\right\}\right)$
38 35 36 37 3imtr4g ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\right)\to \left(\exists !{b}\in {V}\phantom{\rule{.4em}{0ex}}\left\{\left\{{A},{b}\right\},\left\{{b},{C}\right\}\right\}\subseteq {E}\to \exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({G}\mathrm{NeighbVtx}{A}\right)\cap \left({G}\mathrm{NeighbVtx}{C}\right)=\left\{{x}\right\}\right)$
39 4 38 mpd ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\right)\to \exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({G}\mathrm{NeighbVtx}{A}\right)\cap \left({G}\mathrm{NeighbVtx}{C}\right)=\left\{{x}\right\}$
40 39 ex ${⊢}{G}\in \mathrm{FriendGraph}\to \left(\left({A}\in {V}\wedge {C}\in {V}\wedge {A}\ne {C}\right)\to \exists {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({G}\mathrm{NeighbVtx}{A}\right)\cap \left({G}\mathrm{NeighbVtx}{C}\right)=\left\{{x}\right\}\right)$