frgrncvvdeqlem8

Description: Lemma 8 for frgrncvvdeq . This corresponds to statement 2 in Huneke p. 1: "The map is one-to-one since z in N(x) is uniquely determined as the common neighbor of x and a(x)". (Contributed by Alexander van der Vekens, 23-Dec-2017) (Revised by AV, 10-May-2021) (Revised by AV, 30-Dec-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	frgrncvvdeqlem8	$⊢ φ \to A : D \underset{1-1}{⟶} 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	1 2 3 4 5 6 7 8 9 10	frgrncvvdeqlem4	$⊢ φ \to A : D ⟶ N$
12		simpr	$⊢ (φ \land A : D ⟶ N) \to A : D ⟶ N$
13		ffvelcdm	$⊢ (A : D ⟶ N \land u \in D) \to A (u) \in N$
14	13	ad2ant2lr	$⊢ ((φ \land A : D ⟶ N) \land (u \in D \land w \in D)) \to A (u) \in N$
15	14	adantr	$⊢ (((φ \land A : D ⟶ N) \land (u \in D \land w \in D)) \land A (u) = A (w)) \to A (u) \in N$
16	1 2 3 4 5 6 7 8 9 10	frgrncvvdeqlem1	$⊢ φ \to X \notin N$
17		preq1	$⊢ x = u \to \{x, y\} = \{u, y\}$
18	17	eleq1d	$⊢ x = u \to (\{x, y\} \in E \leftrightarrow \{u, y\} \in E)$
19	18	riotabidv	$⊢ x = u \to (ι y \in N \| \{x, y\} \in E) = (ι y \in N \| \{u, y\} \in E)$
20	19	cbvmptv	$⊢ (x \in D ⟼ (ι y \in N \| \{x, y\} \in E)) = (u \in D ⟼ (ι y \in N \| \{u, y\} \in E))$
21	10 20	eqtri	$⊢ A = (u \in D ⟼ (ι y \in N \| \{u, y\} \in E))$
22	1 2 3 4 5 6 7 8 9 21	frgrncvvdeqlem6	$⊢ (φ \land u \in D) \to \{u, A (u)\} \in E$
23		preq1	$⊢ x = w \to \{x, y\} = \{w, y\}$
24	23	eleq1d	$⊢ x = w \to (\{x, y\} \in E \leftrightarrow \{w, y\} \in E)$
25	24	riotabidv	$⊢ x = w \to (ι y \in N \| \{x, y\} \in E) = (ι y \in N \| \{w, y\} \in E)$
26	25	cbvmptv	$⊢ (x \in D ⟼ (ι y \in N \| \{x, y\} \in E)) = (w \in D ⟼ (ι y \in N \| \{w, y\} \in E))$
27	10 26	eqtri	$⊢ A = (w \in D ⟼ (ι y \in N \| \{w, y\} \in E))$
28	1 2 3 4 5 6 7 8 9 27	frgrncvvdeqlem6	$⊢ (φ \land w \in D) \to \{w, A (w)\} \in E$
29	22 28	anim12dan	$⊢ (φ \land (u \in D \land w \in D)) \to (\{u, A (u)\} \in E \land \{w, A (w)\} \in E)$
30		preq2	$⊢ A (w) = A (u) \to \{w, A (w)\} = \{w, A (u)\}$
31	30	eleq1d	$⊢ A (w) = A (u) \to (\{w, A (w)\} \in E \leftrightarrow \{w, A (u)\} \in E)$
32	31	anbi2d	$⊢ A (w) = A (u) \to ((\{u, A (u)\} \in E \land \{w, A (w)\} \in E) \leftrightarrow (\{u, A (u)\} \in E \land \{w, A (u)\} \in E))$
33	32	eqcoms	$⊢ A (u) = A (w) \to ((\{u, A (u)\} \in E \land \{w, A (w)\} \in E) \leftrightarrow (\{u, A (u)\} \in E \land \{w, A (u)\} \in E))$
34	33	biimpa	$⊢ (A (u) = A (w) \land (\{u, A (u)\} \in E \land \{w, A (w)\} \in E)) \to (\{u, A (u)\} \in E \land \{w, A (u)\} \in E)$
35		df-ne	$⊢ u \neq w \leftrightarrow \neg u = w$
36	2 3	frgrnbnb	$⊢ (G \in FriendGraph \land (u \in D \land w \in D) \land u \neq w) \to ((\{u, A (u)\} \in E \land \{w, A (u)\} \in E) \to A (u) = X)$
37	9 36	syl3an1	$⊢ (φ \land (u \in D \land w \in D) \land u \neq w) \to ((\{u, A (u)\} \in E \land \{w, A (u)\} \in E) \to A (u) = X)$
38	37	3expa	$⊢ ((φ \land (u \in D \land w \in D)) \land u \neq w) \to ((\{u, A (u)\} \in E \land \{w, A (u)\} \in E) \to A (u) = X)$
39		df-nel	$⊢ X \notin N \leftrightarrow \neg X \in N$
40		eleq1	$⊢ A (u) = X \to (A (u) \in N \leftrightarrow X \in N)$
41	40	biimpa	$⊢ (A (u) = X \land A (u) \in N) \to X \in N$
42	41	pm2.24d	$⊢ (A (u) = X \land A (u) \in N) \to (\neg X \in N \to u = w)$
43	42	expcom	$⊢ A (u) \in N \to (A (u) = X \to (\neg X \in N \to u = w))$
44	43	com13	$⊢ \neg X \in N \to (A (u) = X \to (A (u) \in N \to u = w))$
45	39 44	sylbi	$⊢ X \notin N \to (A (u) = X \to (A (u) \in N \to u = w))$
46	45	com12	$⊢ A (u) = X \to (X \notin N \to (A (u) \in N \to u = w))$
47	38 46	syl6	$⊢ ((φ \land (u \in D \land w \in D)) \land u \neq w) \to ((\{u, A (u)\} \in E \land \{w, A (u)\} \in E) \to (X \notin N \to (A (u) \in N \to u = w)))$
48	47	expcom	$⊢ u \neq w \to ((φ \land (u \in D \land w \in D)) \to ((\{u, A (u)\} \in E \land \{w, A (u)\} \in E) \to (X \notin N \to (A (u) \in N \to u = w))))$
49	48	com23	$⊢ u \neq w \to ((\{u, A (u)\} \in E \land \{w, A (u)\} \in E) \to ((φ \land (u \in D \land w \in D)) \to (X \notin N \to (A (u) \in N \to u = w))))$
50	35 49	sylbir	$⊢ \neg u = w \to ((\{u, A (u)\} \in E \land \{w, A (u)\} \in E) \to ((φ \land (u \in D \land w \in D)) \to (X \notin N \to (A (u) \in N \to u = w))))$
51	34 50	syl5com	$⊢ (A (u) = A (w) \land (\{u, A (u)\} \in E \land \{w, A (w)\} \in E)) \to (\neg u = w \to ((φ \land (u \in D \land w \in D)) \to (X \notin N \to (A (u) \in N \to u = w))))$
52	51	expcom	$⊢ (\{u, A (u)\} \in E \land \{w, A (w)\} \in E) \to (A (u) = A (w) \to (\neg u = w \to ((φ \land (u \in D \land w \in D)) \to (X \notin N \to (A (u) \in N \to u = w)))))$
53	52	com24	$⊢ (\{u, A (u)\} \in E \land \{w, A (w)\} \in E) \to ((φ \land (u \in D \land w \in D)) \to (\neg u = w \to (A (u) = A (w) \to (X \notin N \to (A (u) \in N \to u = w)))))$
54	29 53	mpcom	$⊢ (φ \land (u \in D \land w \in D)) \to (\neg u = w \to (A (u) = A (w) \to (X \notin N \to (A (u) \in N \to u = w))))$
55	54	ex	$⊢ φ \to ((u \in D \land w \in D) \to (\neg u = w \to (A (u) = A (w) \to (X \notin N \to (A (u) \in N \to u = w)))))$
56	55	com3r	$⊢ \neg u = w \to (φ \to ((u \in D \land w \in D) \to (A (u) = A (w) \to (X \notin N \to (A (u) \in N \to u = w)))))$
57	56	com15	$⊢ X \notin N \to (φ \to ((u \in D \land w \in D) \to (A (u) = A (w) \to (\neg u = w \to (A (u) \in N \to u = w)))))$
58	16 57	mpcom	$⊢ φ \to ((u \in D \land w \in D) \to (A (u) = A (w) \to (\neg u = w \to (A (u) \in N \to u = w))))$
59	58	expd	$⊢ φ \to (u \in D \to (w \in D \to (A (u) = A (w) \to (\neg u = w \to (A (u) \in N \to u = w)))))$
60	59	adantr	$⊢ (φ \land A : D ⟶ N) \to (u \in D \to (w \in D \to (A (u) = A (w) \to (\neg u = w \to (A (u) \in N \to u = w)))))$
61	60	imp42	$⊢ (((φ \land A : D ⟶ N) \land (u \in D \land w \in D)) \land A (u) = A (w)) \to (\neg u = w \to (A (u) \in N \to u = w))$
62	15 61	mpid	$⊢ (((φ \land A : D ⟶ N) \land (u \in D \land w \in D)) \land A (u) = A (w)) \to (\neg u = w \to u = w)$
63	62	pm2.18d	$⊢ (((φ \land A : D ⟶ N) \land (u \in D \land w \in D)) \land A (u) = A (w)) \to u = w$
64	63	ex	$⊢ ((φ \land A : D ⟶ N) \land (u \in D \land w \in D)) \to (A (u) = A (w) \to u = w)$
65	64	ralrimivva	$⊢ (φ \land A : D ⟶ N) \to \forall u \in D \forall w \in D (A (u) = A (w) \to u = w)$
66		dff13	$⊢ A : D \underset{1-1}{⟶} N \leftrightarrow (A : D ⟶ N \land \forall u \in D \forall w \in D (A (u) = A (w) \to u = w))$
67	12 65 66	sylanbrc	$⊢ (φ \land A : D ⟶ N) \to A : D \underset{1-1}{⟶} N$
68	11 67	mpdan	$⊢ φ \to A : D \underset{1-1}{⟶} N$

Metamath Proof Explorer

Theorem frgrncvvdeqlem8

Proof