frgrncvvdeqlem7

Description: Lemma 7 for frgrncvvdeq . This corresponds to statement 1 in Huneke p. 1: "This common neighbor cannot be x, as x and y are not adjacent.". This is only an observation, which is not required to proof the friendship theorem. (Contributed by Alexander van der Vekens, 23-Dec-2017) (Revised by AV, 10-May-2021)

	Ref	Expression
Hypotheses	frgrncvvdeq.v1	$⊢ V = Vtx (G)$
	frgrncvvdeq.e	$⊢ E = Edg (G)$
	frgrncvvdeq.nx	$⊢ D = G NeighbVtx X$
	frgrncvvdeq.ny	$⊢ N = G NeighbVtx Y$
	frgrncvvdeq.x	$⊢ φ \to X \in V$
	frgrncvvdeq.y	$⊢ φ \to Y \in V$
	frgrncvvdeq.ne	$⊢ φ \to X \neq Y$
	frgrncvvdeq.xy	$⊢ φ \to Y \notin D$
	frgrncvvdeq.f	$⊢ φ \to G \in FriendGraph$
	frgrncvvdeq.a	$⊢ A = (x \in D ⟼ (ι y \in N \| \{x, y\} \in E))$
Assertion	frgrncvvdeqlem7	$⊢ φ \to \forall x \in D A (x) \neq X$

Proof

Step	Hyp	Ref	Expression
1		frgrncvvdeq.v1	$⊢ V = Vtx (G)$
2		frgrncvvdeq.e	$⊢ E = Edg (G)$
3		frgrncvvdeq.nx	$⊢ D = G NeighbVtx X$
4		frgrncvvdeq.ny	$⊢ N = G NeighbVtx Y$
5		frgrncvvdeq.x	$⊢ φ \to X \in V$
6		frgrncvvdeq.y	$⊢ φ \to Y \in V$
7		frgrncvvdeq.ne	$⊢ φ \to X \neq Y$
8		frgrncvvdeq.xy	$⊢ φ \to Y \notin D$
9		frgrncvvdeq.f	$⊢ φ \to G \in FriendGraph$
10		frgrncvvdeq.a	$⊢ A = (x \in D ⟼ (ι y \in N \| \{x, y\} \in E))$
11	1 2 3 4 5 6 7 8 9 10	frgrncvvdeqlem5	$⊢ (φ \land x \in D) \to \{A (x)\} = (G NeighbVtx x) \cap N$
12		fvex	$⊢ A (x) \in V$
13	12	snid	$⊢ A (x) \in \{A (x)\}$
14		eleq2	$⊢ \{A (x)\} = (G NeighbVtx x) \cap N \to (A (x) \in \{A (x)\} \leftrightarrow A (x) \in ((G NeighbVtx x) \cap N))$
15	14	biimpa	$⊢ (\{A (x)\} = (G NeighbVtx x) \cap N \land A (x) \in \{A (x)\}) \to A (x) \in ((G NeighbVtx x) \cap N)$
16		elin	$⊢ A (x) \in ((G NeighbVtx x) \cap N) \leftrightarrow (A (x) \in (G NeighbVtx x) \land A (x) \in N)$
17	1 2 3 4 5 6 7 8 9 10	frgrncvvdeqlem1	$⊢ φ \to X \notin N$
18		df-nel	$⊢ X \notin N \leftrightarrow \neg X \in N$
19		nelelne	$⊢ \neg X \in N \to (A (x) \in N \to A (x) \neq X)$
20	18 19	sylbi	$⊢ X \notin N \to (A (x) \in N \to A (x) \neq X)$
21	17 20	syl	$⊢ φ \to (A (x) \in N \to A (x) \neq X)$
22	21	adantr	$⊢ (φ \land x \in D) \to (A (x) \in N \to A (x) \neq X)$
23	22	com12	$⊢ A (x) \in N \to ((φ \land x \in D) \to A (x) \neq X)$
24	16 23	simplbiim	$⊢ A (x) \in ((G NeighbVtx x) \cap N) \to ((φ \land x \in D) \to A (x) \neq X)$
25	15 24	syl	$⊢ (\{A (x)\} = (G NeighbVtx x) \cap N \land A (x) \in \{A (x)\}) \to ((φ \land x \in D) \to A (x) \neq X)$
26	13 25	mpan2	$⊢ \{A (x)\} = (G NeighbVtx x) \cap N \to ((φ \land x \in D) \to A (x) \neq X)$
27	11 26	mpcom	$⊢ (φ \land x \in D) \to A (x) \neq X$
28	27	ralrimiva	$⊢ φ \to \forall x \in D A (x) \neq X$

Metamath Proof Explorer

Theorem frgrncvvdeqlem7

Proof