# 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 𝑉 = ( Vtx ‘ 𝐺 )
frcond1.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion frcond4 ( 𝐺 ∈ FriendGraph → ∀ 𝑘𝑉𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃ 𝑥𝑉 ( ( 𝐺 NeighbVtx 𝑘 ) ∩ ( 𝐺 NeighbVtx 𝑙 ) ) = { 𝑥 } )

### Proof

Step Hyp Ref Expression
1 frcond1.v 𝑉 = ( Vtx ‘ 𝐺 )
2 frcond1.e 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 frcond3 ( 𝐺 ∈ FriendGraph → ( ( 𝑘𝑉𝑙𝑉𝑘𝑙 ) → ∃ 𝑥𝑉 ( ( 𝐺 NeighbVtx 𝑘 ) ∩ ( 𝐺 NeighbVtx 𝑙 ) ) = { 𝑥 } ) )
4 eldifsn ( 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ↔ ( 𝑙𝑉𝑙𝑘 ) )
5 necom ( 𝑙𝑘𝑘𝑙 )
6 5 biimpi ( 𝑙𝑘𝑘𝑙 )
7 6 anim2i ( ( 𝑙𝑉𝑙𝑘 ) → ( 𝑙𝑉𝑘𝑙 ) )
8 4 7 sylbi ( 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) → ( 𝑙𝑉𝑘𝑙 ) )
9 8 anim2i ( ( 𝑘𝑉𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ) → ( 𝑘𝑉 ∧ ( 𝑙𝑉𝑘𝑙 ) ) )
10 3anass ( ( 𝑘𝑉𝑙𝑉𝑘𝑙 ) ↔ ( 𝑘𝑉 ∧ ( 𝑙𝑉𝑘𝑙 ) ) )
11 9 10 sylibr ( ( 𝑘𝑉𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ) → ( 𝑘𝑉𝑙𝑉𝑘𝑙 ) )
12 3 11 impel ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑘𝑉𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ) ) → ∃ 𝑥𝑉 ( ( 𝐺 NeighbVtx 𝑘 ) ∩ ( 𝐺 NeighbVtx 𝑙 ) ) = { 𝑥 } )
13 12 ralrimivva ( 𝐺 ∈ FriendGraph → ∀ 𝑘𝑉𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃ 𝑥𝑉 ( ( 𝐺 NeighbVtx 𝑘 ) ∩ ( 𝐺 NeighbVtx 𝑙 ) ) = { 𝑥 } )