frgrncvvdeqlem1

Description: Lemma 1 for frgrncvvdeq . (Contributed by Alexander van der Vekens, 23-Dec-2017) (Revised by AV, 8-May-2021) (Proof shortened by AV, 12-Feb-2022)

	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	frgrncvvdeqlem1	$⊢ φ \to X \notin N$

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		df-nel	$⊢ Y \notin D \leftrightarrow \neg Y \in D$
12	3	eleq2i	$⊢ Y \in D \leftrightarrow Y \in (G NeighbVtx X)$
13	11 12	xchbinx	$⊢ Y \notin D \leftrightarrow \neg Y \in (G NeighbVtx X)$
14	8 13	sylib	$⊢ φ \to \neg Y \in (G NeighbVtx X)$
15		nbgrsym	$⊢ X \in (G NeighbVtx Y) \leftrightarrow Y \in (G NeighbVtx X)$
16	14 15	sylnibr	$⊢ φ \to \neg X \in (G NeighbVtx Y)$
17		neleq2	$⊢ N = G NeighbVtx Y \to (X \notin N \leftrightarrow X \notin (G NeighbVtx Y))$
18	4 17	ax-mp	$⊢ X \notin N \leftrightarrow X \notin (G NeighbVtx Y)$
19		df-nel	$⊢ X \notin (G NeighbVtx Y) \leftrightarrow \neg X \in (G NeighbVtx Y)$
20	18 19	bitri	$⊢ X \notin N \leftrightarrow \neg X \in (G NeighbVtx Y)$
21	16 20	sylibr	$⊢ φ \to X \notin N$

Metamath Proof Explorer

Theorem frgrncvvdeqlem1

Proof