# Metamath Proof Explorer

## Theorem frgrnbnb

Description: If two neighbors U and W of a vertex X have a common neighbor A in a friendship graph, then this common neighbor A must be the vertex X . (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 2-Apr-2021) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypotheses frgrnbnb.e $⊢ E = Edg ⁡ G$
frgrnbnb.n $⊢ D = G NeighbVtx X$
Assertion frgrnbnb $⊢ G ∈ FriendGraph ∧ U ∈ D ∧ W ∈ D ∧ U ≠ W → U A ∈ E ∧ W A ∈ E → A = X$

### Proof

Step Hyp Ref Expression
1 frgrnbnb.e $⊢ E = Edg ⁡ G$
2 frgrnbnb.n $⊢ D = G NeighbVtx X$
3 frgrusgr $⊢ G ∈ FriendGraph → G ∈ USGraph$
4 2 eleq2i $⊢ U ∈ D ↔ U ∈ G NeighbVtx X$
5 1 nbusgreledg $⊢ G ∈ USGraph → U ∈ G NeighbVtx X ↔ U X ∈ E$
6 5 biimpd $⊢ G ∈ USGraph → U ∈ G NeighbVtx X → U X ∈ E$
7 4 6 syl5bi $⊢ G ∈ USGraph → U ∈ D → U X ∈ E$
8 2 eleq2i $⊢ W ∈ D ↔ W ∈ G NeighbVtx X$
9 1 nbusgreledg $⊢ G ∈ USGraph → W ∈ G NeighbVtx X ↔ W X ∈ E$
10 9 biimpd $⊢ G ∈ USGraph → W ∈ G NeighbVtx X → W X ∈ E$
11 8 10 syl5bi $⊢ G ∈ USGraph → W ∈ D → W X ∈ E$
12 7 11 anim12d $⊢ G ∈ USGraph → U ∈ D ∧ W ∈ D → U X ∈ E ∧ W X ∈ E$
13 12 imp $⊢ G ∈ USGraph ∧ U ∈ D ∧ W ∈ D → U X ∈ E ∧ W X ∈ E$
14 eqid $⊢ Vtx ⁡ G = Vtx ⁡ G$
15 14 nbgrisvtx $⊢ U ∈ G NeighbVtx X → U ∈ Vtx ⁡ G$
16 15 2 eleq2s $⊢ U ∈ D → U ∈ Vtx ⁡ G$
17 14 nbgrisvtx $⊢ W ∈ G NeighbVtx X → W ∈ Vtx ⁡ G$
18 17 2 eleq2s $⊢ W ∈ D → W ∈ Vtx ⁡ G$
19 16 18 anim12i $⊢ U ∈ D ∧ W ∈ D → U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G$
20 19 adantl $⊢ G ∈ USGraph ∧ U ∈ D ∧ W ∈ D → U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G$
21 1 14 usgrpredgv $⊢ G ∈ USGraph ∧ U A ∈ E → U ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G$
22 21 ad2ant2r $⊢ G ∈ USGraph ∧ U ∈ D ∧ W ∈ D ∧ U A ∈ E ∧ W A ∈ E → U ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G$
23 ax-1 $⊢ A = X → G ∈ FriendGraph → A = X$
24 23 2a1d $⊢ A = X → U A ∈ E ∧ W A ∈ E → X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → G ∈ FriendGraph → A = X$
25 24 2a1d $⊢ A = X → U ≠ W → U X ∈ E ∧ W X ∈ E → U A ∈ E ∧ W A ∈ E → X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → G ∈ FriendGraph → A = X$
26 simpll $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ A ≠ X ∧ U ≠ W → G ∈ USGraph$
27 simprrr $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → W ∈ Vtx ⁡ G$
28 27 adantr $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ A ≠ X ∧ U ≠ W → W ∈ Vtx ⁡ G$
29 simprrl $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → U ∈ Vtx ⁡ G$
30 29 adantr $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ A ≠ X ∧ U ≠ W → U ∈ Vtx ⁡ G$
31 necom $⊢ U ≠ W ↔ W ≠ U$
32 31 biimpi $⊢ U ≠ W → W ≠ U$
33 32 adantl $⊢ A ≠ X ∧ U ≠ W → W ≠ U$
34 33 adantl $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ A ≠ X ∧ U ≠ W → W ≠ U$
35 28 30 34 3jca $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ A ≠ X ∧ U ≠ W → W ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ≠ U$
36 simprll $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → X ∈ Vtx ⁡ G$
37 36 adantr $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ A ≠ X ∧ U ≠ W → X ∈ Vtx ⁡ G$
38 simprlr $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → A ∈ Vtx ⁡ G$
39 38 adantr $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ A ≠ X ∧ U ≠ W → A ∈ Vtx ⁡ G$
40 necom $⊢ A ≠ X ↔ X ≠ A$
41 40 biimpi $⊢ A ≠ X → X ≠ A$
42 41 adantr $⊢ A ≠ X ∧ U ≠ W → X ≠ A$
43 42 adantl $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ A ≠ X ∧ U ≠ W → X ≠ A$
44 37 39 43 3jca $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ A ≠ X ∧ U ≠ W → X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ X ≠ A$
45 26 35 44 3jca $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ A ≠ X ∧ U ≠ W → G ∈ USGraph ∧ W ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ≠ U ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ X ≠ A$
46 45 ad4ant14 $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ U X ∈ E ∧ W X ∈ E ∧ U A ∈ E ∧ W A ∈ E ∧ A ≠ X ∧ U ≠ W → G ∈ USGraph ∧ W ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ≠ U ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ X ≠ A$
47 prcom $⊢ U X = X U$
48 47 eleq1i $⊢ U X ∈ E ↔ X U ∈ E$
49 48 biimpi $⊢ U X ∈ E → X U ∈ E$
50 49 anim1ci $⊢ U X ∈ E ∧ W X ∈ E → W X ∈ E ∧ X U ∈ E$
51 50 adantl $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ U X ∈ E ∧ W X ∈ E → W X ∈ E ∧ X U ∈ E$
52 prcom $⊢ W A = A W$
53 52 eleq1i $⊢ W A ∈ E ↔ A W ∈ E$
54 53 biimpi $⊢ W A ∈ E → A W ∈ E$
55 54 anim2i $⊢ U A ∈ E ∧ W A ∈ E → U A ∈ E ∧ A W ∈ E$
56 51 55 anim12i $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ U X ∈ E ∧ W X ∈ E ∧ U A ∈ E ∧ W A ∈ E → W X ∈ E ∧ X U ∈ E ∧ U A ∈ E ∧ A W ∈ E$
57 56 adantr $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ U X ∈ E ∧ W X ∈ E ∧ U A ∈ E ∧ W A ∈ E ∧ A ≠ X ∧ U ≠ W → W X ∈ E ∧ X U ∈ E ∧ U A ∈ E ∧ A W ∈ E$
58 14 1 4cyclusnfrgr $⊢ G ∈ USGraph ∧ W ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ≠ U ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ X ≠ A → W X ∈ E ∧ X U ∈ E ∧ U A ∈ E ∧ A W ∈ E → G ∉ FriendGraph$
59 46 57 58 sylc $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ U X ∈ E ∧ W X ∈ E ∧ U A ∈ E ∧ W A ∈ E ∧ A ≠ X ∧ U ≠ W → G ∉ FriendGraph$
60 df-nel $⊢ G ∉ FriendGraph ↔ ¬ G ∈ FriendGraph$
61 59 60 sylib $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ U X ∈ E ∧ W X ∈ E ∧ U A ∈ E ∧ W A ∈ E ∧ A ≠ X ∧ U ≠ W → ¬ G ∈ FriendGraph$
62 61 pm2.21d $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ U X ∈ E ∧ W X ∈ E ∧ U A ∈ E ∧ W A ∈ E ∧ A ≠ X ∧ U ≠ W → G ∈ FriendGraph → A = X$
63 62 ex $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ U X ∈ E ∧ W X ∈ E ∧ U A ∈ E ∧ W A ∈ E → A ≠ X ∧ U ≠ W → G ∈ FriendGraph → A = X$
64 63 com23 $⊢ G ∈ USGraph ∧ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G ∧ U X ∈ E ∧ W X ∈ E ∧ U A ∈ E ∧ W A ∈ E → G ∈ FriendGraph → A ≠ X ∧ U ≠ W → A = X$
65 64 exp41 $⊢ G ∈ USGraph → X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → U X ∈ E ∧ W X ∈ E → U A ∈ E ∧ W A ∈ E → G ∈ FriendGraph → A ≠ X ∧ U ≠ W → A = X$
66 65 com25 $⊢ G ∈ USGraph → G ∈ FriendGraph → U X ∈ E ∧ W X ∈ E → U A ∈ E ∧ W A ∈ E → X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → A ≠ X ∧ U ≠ W → A = X$
67 3 66 mpcom $⊢ G ∈ FriendGraph → U X ∈ E ∧ W X ∈ E → U A ∈ E ∧ W A ∈ E → X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → A ≠ X ∧ U ≠ W → A = X$
68 67 com15 $⊢ A ≠ X ∧ U ≠ W → U X ∈ E ∧ W X ∈ E → U A ∈ E ∧ W A ∈ E → X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → G ∈ FriendGraph → A = X$
69 68 ex $⊢ A ≠ X → U ≠ W → U X ∈ E ∧ W X ∈ E → U A ∈ E ∧ W A ∈ E → X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → G ∈ FriendGraph → A = X$
70 25 69 pm2.61ine $⊢ U ≠ W → U X ∈ E ∧ W X ∈ E → U A ∈ E ∧ W A ∈ E → X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → G ∈ FriendGraph → A = X$
71 70 imp $⊢ U ≠ W ∧ U X ∈ E ∧ W X ∈ E → U A ∈ E ∧ W A ∈ E → X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → G ∈ FriendGraph → A = X$
72 71 com13 $⊢ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → U A ∈ E ∧ W A ∈ E → U ≠ W ∧ U X ∈ E ∧ W X ∈ E → G ∈ FriendGraph → A = X$
73 72 ex $⊢ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G → U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → U A ∈ E ∧ W A ∈ E → U ≠ W ∧ U X ∈ E ∧ W X ∈ E → G ∈ FriendGraph → A = X$
74 73 com25 $⊢ X ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G → G ∈ FriendGraph → U A ∈ E ∧ W A ∈ E → U ≠ W ∧ U X ∈ E ∧ W X ∈ E → U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → A = X$
75 74 ex $⊢ X ∈ Vtx ⁡ G → A ∈ Vtx ⁡ G → G ∈ FriendGraph → U A ∈ E ∧ W A ∈ E → U ≠ W ∧ U X ∈ E ∧ W X ∈ E → U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → A = X$
76 14 nbgrcl $⊢ U ∈ G NeighbVtx X → X ∈ Vtx ⁡ G$
77 76 2 eleq2s $⊢ U ∈ D → X ∈ Vtx ⁡ G$
78 77 adantr $⊢ U ∈ D ∧ W ∈ D → X ∈ Vtx ⁡ G$
79 78 adantl $⊢ G ∈ USGraph ∧ U ∈ D ∧ W ∈ D → X ∈ Vtx ⁡ G$
80 75 79 syl11 $⊢ A ∈ Vtx ⁡ G → G ∈ USGraph ∧ U ∈ D ∧ W ∈ D → G ∈ FriendGraph → U A ∈ E ∧ W A ∈ E → U ≠ W ∧ U X ∈ E ∧ W X ∈ E → U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → A = X$
81 80 com34 $⊢ A ∈ Vtx ⁡ G → G ∈ USGraph ∧ U ∈ D ∧ W ∈ D → U A ∈ E ∧ W A ∈ E → G ∈ FriendGraph → U ≠ W ∧ U X ∈ E ∧ W X ∈ E → U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → A = X$
82 81 impd $⊢ A ∈ Vtx ⁡ G → G ∈ USGraph ∧ U ∈ D ∧ W ∈ D ∧ U A ∈ E ∧ W A ∈ E → G ∈ FriendGraph → U ≠ W ∧ U X ∈ E ∧ W X ∈ E → U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → A = X$
83 82 adantl $⊢ U ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G → G ∈ USGraph ∧ U ∈ D ∧ W ∈ D ∧ U A ∈ E ∧ W A ∈ E → G ∈ FriendGraph → U ≠ W ∧ U X ∈ E ∧ W X ∈ E → U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → A = X$
84 22 83 mpcom $⊢ G ∈ USGraph ∧ U ∈ D ∧ W ∈ D ∧ U A ∈ E ∧ W A ∈ E → G ∈ FriendGraph → U ≠ W ∧ U X ∈ E ∧ W X ∈ E → U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → A = X$
85 84 ex $⊢ G ∈ USGraph ∧ U ∈ D ∧ W ∈ D → U A ∈ E ∧ W A ∈ E → G ∈ FriendGraph → U ≠ W ∧ U X ∈ E ∧ W X ∈ E → U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → A = X$
86 85 com25 $⊢ G ∈ USGraph ∧ U ∈ D ∧ W ∈ D → U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → G ∈ FriendGraph → U ≠ W ∧ U X ∈ E ∧ W X ∈ E → U A ∈ E ∧ W A ∈ E → A = X$
87 86 com14 $⊢ U ≠ W ∧ U X ∈ E ∧ W X ∈ E → U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → G ∈ FriendGraph → G ∈ USGraph ∧ U ∈ D ∧ W ∈ D → U A ∈ E ∧ W A ∈ E → A = X$
88 87 ex $⊢ U ≠ W → U X ∈ E ∧ W X ∈ E → U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → G ∈ FriendGraph → G ∈ USGraph ∧ U ∈ D ∧ W ∈ D → U A ∈ E ∧ W A ∈ E → A = X$
89 88 com15 $⊢ G ∈ USGraph ∧ U ∈ D ∧ W ∈ D → U X ∈ E ∧ W X ∈ E → U ∈ Vtx ⁡ G ∧ W ∈ Vtx ⁡ G → G ∈ FriendGraph → U ≠ W → U A ∈ E ∧ W A ∈ E → A = X$
90 13 20 89 mp2d $⊢ G ∈ USGraph ∧ U ∈ D ∧ W ∈ D → G ∈ FriendGraph → U ≠ W → U A ∈ E ∧ W A ∈ E → A = X$
91 90 ex $⊢ G ∈ USGraph → U ∈ D ∧ W ∈ D → G ∈ FriendGraph → U ≠ W → U A ∈ E ∧ W A ∈ E → A = X$
92 91 com23 $⊢ G ∈ USGraph → G ∈ FriendGraph → U ∈ D ∧ W ∈ D → U ≠ W → U A ∈ E ∧ W A ∈ E → A = X$
93 3 92 mpcom $⊢ G ∈ FriendGraph → U ∈ D ∧ W ∈ D → U ≠ W → U A ∈ E ∧ W A ∈ E → A = X$
94 93 3imp $⊢ G ∈ FriendGraph ∧ U ∈ D ∧ W ∈ D ∧ U ≠ W → U A ∈ E ∧ W A ∈ E → A = X$