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 \in FriendGraph \to \forall k \in V \forall l \in (V ∖ \{k\}) \exists x \in V (G NeighbVtx k) \cap (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 \in FriendGraph \to ((k \in V \land l \in V \land k \neq l) \to \exists x \in V (G NeighbVtx k) \cap (G NeighbVtx l) = \{x\})$
4		eldifsn	$⊢ l \in (V ∖ \{k\}) \leftrightarrow (l \in V \land l \neq k)$
5		necom	$⊢ l \neq k \leftrightarrow k \neq l$
6	5	biimpi	$⊢ l \neq k \to k \neq l$
7	6	anim2i	$⊢ (l \in V \land l \neq k) \to (l \in V \land k \neq l)$
8	4 7	sylbi	$⊢ l \in (V ∖ \{k\}) \to (l \in V \land k \neq l)$
9	8	anim2i	$⊢ (k \in V \land l \in (V ∖ \{k\})) \to (k \in V \land (l \in V \land k \neq l))$
10		3anass	$⊢ (k \in V \land l \in V \land k \neq l) \leftrightarrow (k \in V \land (l \in V \land k \neq l))$
11	9 10	sylibr	$⊢ (k \in V \land l \in (V ∖ \{k\})) \to (k \in V \land l \in V \land k \neq l)$
12	3 11	impel	$⊢ (G \in FriendGraph \land (k \in V \land l \in (V ∖ \{k\}))) \to \exists x \in V (G NeighbVtx k) \cap (G NeighbVtx l) = \{x\}$
13	12	ralrimivva	$⊢ G \in FriendGraph \to \forall k \in V \forall l \in (V ∖ \{k\}) \exists x \in V (G NeighbVtx k) \cap (G NeighbVtx l) = \{x\}$

Metamath Proof Explorer

Theorem frcond4

Proof