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 = Vtx ⁡ G
frcond1.e ⊢ E = Edg ⁡ G
Assertion frcond4 ⊢ G ∈ FriendGraph → ∀ k ∈ V ∀ l ∈ V ∖ k ∃ x ∈ V G NeighbVtx k ∩ G NeighbVtx l = x

Proof

Step Hyp Ref Expression
1 frcond1.v ⊢ V = Vtx ⁡ G
2 frcond1.e ⊢ E = Edg ⁡ G
3 1 2 frcond3 ⊢ G ∈ FriendGraph → k ∈ V ∧ l ∈ V ∧ k ≠ l → ∃ x ∈ V G NeighbVtx k ∩ G NeighbVtx l = x
4 eldifsn ⊢ l ∈ V ∖ k ↔ l ∈ V ∧ l ≠ k
5 necom ⊢ l ≠ k ↔ k ≠ l
6 5 biimpi ⊢ l ≠ k → k ≠ l
7 6 anim2i ⊢ l ∈ V ∧ l ≠ k → l ∈ V ∧ k ≠ l
8 4 7 sylbi ⊢ l ∈ V ∖ k → l ∈ V ∧ k ≠ l
9 8 anim2i ⊢ k ∈ V ∧ l ∈ V ∖ k → k ∈ V ∧ l ∈ V ∧ k ≠ l
10 3anass ⊢ k ∈ V ∧ l ∈ V ∧ k ≠ l ↔ k ∈ V ∧ l ∈ V ∧ k ≠ l
11 9 10 sylibr ⊢ k ∈ V ∧ l ∈ V ∖ k → k ∈ V ∧ l ∈ V ∧ k ≠ l
12 3 11 impel ⊢ G ∈ FriendGraph ∧ k ∈ V ∧ l ∈ V ∖ k → ∃ x ∈ V G NeighbVtx k ∩ G NeighbVtx l = x
13 12 ralrimivva ⊢ G ∈ FriendGraph → ∀ k ∈ V ∀ l ∈ V ∖ k ∃ x ∈ V G NeighbVtx k ∩ G NeighbVtx l = x