frgrncvvdeqlem3

Description: Lemma 3 for frgrncvvdeq . The unique neighbor of a vertex (expressed by a restricted iota) is the intersection of the corresponding neighborhoods. (Contributed by Alexander van der Vekens, 18-Dec-2017) (Revised by AV, 10-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	frgrncvvdeqlem3	$⊢ (φ \land x \in D) \to \{(ι y \in N \| \{x, y\} \in E)\} = (G NeighbVtx x) \cap 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	4	ineq2i	$⊢ (G NeighbVtx x) \cap N = (G NeighbVtx x) \cap (G NeighbVtx Y)$
12	9	adantr	$⊢ (φ \land x \in D) \to G \in FriendGraph$
13	3	eleq2i	$⊢ x \in D \leftrightarrow x \in (G NeighbVtx X)$
14	1	nbgrisvtx	$⊢ x \in (G NeighbVtx X) \to x \in V$
15	14	a1i	$⊢ φ \to (x \in (G NeighbVtx X) \to x \in V)$
16	13 15	biimtrid	$⊢ φ \to (x \in D \to x \in V)$
17	16	imp	$⊢ (φ \land x \in D) \to x \in V$
18	6	adantr	$⊢ (φ \land x \in D) \to Y \in V$
19		elnelne2	$⊢ (x \in D \land Y \notin D) \to x \neq Y$
20	8 19	sylan2	$⊢ (x \in D \land φ) \to x \neq Y$
21	20	ancoms	$⊢ (φ \land x \in D) \to x \neq Y$
22	17 18 21	3jca	$⊢ (φ \land x \in D) \to (x \in V \land Y \in V \land x \neq Y)$
23	1 2	frcond3	$⊢ G \in FriendGraph \to ((x \in V \land Y \in V \land x \neq Y) \to \exists n \in V (G NeighbVtx x) \cap (G NeighbVtx Y) = \{n\})$
24	12 22 23	sylc	$⊢ (φ \land x \in D) \to \exists n \in V (G NeighbVtx x) \cap (G NeighbVtx Y) = \{n\}$
25		vex	$⊢ n \in V$
26		elinsn	$⊢ (n \in V \land (G NeighbVtx x) \cap (G NeighbVtx Y) = \{n\}) \to (n \in (G NeighbVtx x) \land n \in (G NeighbVtx Y))$
27	25 26	mpan	$⊢ (G NeighbVtx x) \cap (G NeighbVtx Y) = \{n\} \to (n \in (G NeighbVtx x) \land n \in (G NeighbVtx Y))$
28		frgrusgr	$⊢ G \in FriendGraph \to G \in USGraph$
29	2	nbusgreledg	$⊢ G \in USGraph \to (n \in (G NeighbVtx x) \leftrightarrow \{n, x\} \in E)$
30		prcom	$⊢ \{n, x\} = \{x, n\}$
31	30	eleq1i	$⊢ \{n, x\} \in E \leftrightarrow \{x, n\} \in E$
32	29 31	bitrdi	$⊢ G \in USGraph \to (n \in (G NeighbVtx x) \leftrightarrow \{x, n\} \in E)$
33	32	biimpd	$⊢ G \in USGraph \to (n \in (G NeighbVtx x) \to \{x, n\} \in E)$
34	9 28 33	3syl	$⊢ φ \to (n \in (G NeighbVtx x) \to \{x, n\} \in E)$
35	34	adantr	$⊢ (φ \land x \in D) \to (n \in (G NeighbVtx x) \to \{x, n\} \in E)$
36	35	com12	$⊢ n \in (G NeighbVtx x) \to ((φ \land x \in D) \to \{x, n\} \in E)$
37	36	adantr	$⊢ (n \in (G NeighbVtx x) \land n \in (G NeighbVtx Y)) \to ((φ \land x \in D) \to \{x, n\} \in E)$
38	37	imp	$⊢ ((n \in (G NeighbVtx x) \land n \in (G NeighbVtx Y)) \land (φ \land x \in D)) \to \{x, n\} \in E$
39	4	eqcomi	$⊢ G NeighbVtx Y = N$
40	39	eleq2i	$⊢ n \in (G NeighbVtx Y) \leftrightarrow n \in N$
41	40	bilani	$⊢ (n \in (G NeighbVtx x) \land n \in (G NeighbVtx Y)) \to n \in N$
42	1 2 3 4 5 6 7 8 9 10	frgrncvvdeqlem2	$⊢ (φ \land x \in D) \to \exists! y \in N \{x, y\} \in E$
43		preq2	$⊢ y = n \to \{x, y\} = \{x, n\}$
44	43	eleq1d	$⊢ y = n \to (\{x, y\} \in E \leftrightarrow \{x, n\} \in E)$
45	44	riota2	$⊢ (n \in N \land \exists! y \in N \{x, y\} \in E) \to (\{x, n\} \in E \leftrightarrow (ι y \in N \| \{x, y\} \in E) = n)$
46	41 42 45	syl2an	$⊢ ((n \in (G NeighbVtx x) \land n \in (G NeighbVtx Y)) \land (φ \land x \in D)) \to (\{x, n\} \in E \leftrightarrow (ι y \in N \| \{x, y\} \in E) = n)$
47	38 46	mpbid	$⊢ ((n \in (G NeighbVtx x) \land n \in (G NeighbVtx Y)) \land (φ \land x \in D)) \to (ι y \in N \| \{x, y\} \in E) = n$
48	27 47	sylan	$⊢ ((G NeighbVtx x) \cap (G NeighbVtx Y) = \{n\} \land (φ \land x \in D)) \to (ι y \in N \| \{x, y\} \in E) = n$
49	48	eqcomd	$⊢ ((G NeighbVtx x) \cap (G NeighbVtx Y) = \{n\} \land (φ \land x \in D)) \to n = (ι y \in N \| \{x, y\} \in E)$
50	49	sneqd	$⊢ ((G NeighbVtx x) \cap (G NeighbVtx Y) = \{n\} \land (φ \land x \in D)) \to \{n\} = \{(ι y \in N \| \{x, y\} \in E)\}$
51		eqeq1	$⊢ (G NeighbVtx x) \cap (G NeighbVtx Y) = \{n\} \to ((G NeighbVtx x) \cap (G NeighbVtx Y) = \{(ι y \in N \| \{x, y\} \in E)\} \leftrightarrow \{n\} = \{(ι y \in N \| \{x, y\} \in E)\})$
52	51	adantr	$⊢ ((G NeighbVtx x) \cap (G NeighbVtx Y) = \{n\} \land (φ \land x \in D)) \to ((G NeighbVtx x) \cap (G NeighbVtx Y) = \{(ι y \in N \| \{x, y\} \in E)\} \leftrightarrow \{n\} = \{(ι y \in N \| \{x, y\} \in E)\})$
53	50 52	mpbird	$⊢ ((G NeighbVtx x) \cap (G NeighbVtx Y) = \{n\} \land (φ \land x \in D)) \to (G NeighbVtx x) \cap (G NeighbVtx Y) = \{(ι y \in N \| \{x, y\} \in E)\}$
54	53	ex	$⊢ (G NeighbVtx x) \cap (G NeighbVtx Y) = \{n\} \to ((φ \land x \in D) \to (G NeighbVtx x) \cap (G NeighbVtx Y) = \{(ι y \in N \| \{x, y\} \in E)\})$
55	54	rexlimivw	$⊢ \exists n \in V (G NeighbVtx x) \cap (G NeighbVtx Y) = \{n\} \to ((φ \land x \in D) \to (G NeighbVtx x) \cap (G NeighbVtx Y) = \{(ι y \in N \| \{x, y\} \in E)\})$
56	24 55	mpcom	$⊢ (φ \land x \in D) \to (G NeighbVtx x) \cap (G NeighbVtx Y) = \{(ι y \in N \| \{x, y\} \in E)\}$
57	11 56	eqtr2id	$⊢ (φ \land x \in D) \to \{(ι y \in N \| \{x, y\} \in E)\} = (G NeighbVtx x) \cap N$

Metamath Proof Explorer

Theorem frgrncvvdeqlem3

Proof