# Metamath Proof Explorer

## Theorem 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}=\mathrm{Vtx}\left({G}\right)$
frgrncvvdeq.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
frgrncvvdeq.nx ${⊢}{D}={G}\mathrm{NeighbVtx}{X}$
frgrncvvdeq.ny ${⊢}{N}={G}\mathrm{NeighbVtx}{Y}$
frgrncvvdeq.x ${⊢}{\phi }\to {X}\in {V}$
frgrncvvdeq.y ${⊢}{\phi }\to {Y}\in {V}$
frgrncvvdeq.ne ${⊢}{\phi }\to {X}\ne {Y}$
frgrncvvdeq.xy ${⊢}{\phi }\to {Y}\notin {D}$
frgrncvvdeq.f ${⊢}{\phi }\to {G}\in \mathrm{FriendGraph}$
frgrncvvdeq.a ${⊢}{A}=\left({x}\in {D}⟼\left(\iota {y}\in {N}|\left\{{x},{y}\right\}\in {E}\right)\right)$
Assertion frgrncvvdeqlem8 ${⊢}{\phi }\to {A}:{D}\underset{1-1}{⟶}{N}$

### Proof

Step Hyp Ref Expression
1 frgrncvvdeq.v1 ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 frgrncvvdeq.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 frgrncvvdeq.nx ${⊢}{D}={G}\mathrm{NeighbVtx}{X}$
4 frgrncvvdeq.ny ${⊢}{N}={G}\mathrm{NeighbVtx}{Y}$
5 frgrncvvdeq.x ${⊢}{\phi }\to {X}\in {V}$
6 frgrncvvdeq.y ${⊢}{\phi }\to {Y}\in {V}$
7 frgrncvvdeq.ne ${⊢}{\phi }\to {X}\ne {Y}$
8 frgrncvvdeq.xy ${⊢}{\phi }\to {Y}\notin {D}$
9 frgrncvvdeq.f ${⊢}{\phi }\to {G}\in \mathrm{FriendGraph}$
10 frgrncvvdeq.a ${⊢}{A}=\left({x}\in {D}⟼\left(\iota {y}\in {N}|\left\{{x},{y}\right\}\in {E}\right)\right)$
11 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem4 ${⊢}{\phi }\to {A}:{D}⟶{N}$
12 simpr ${⊢}\left({\phi }\wedge {A}:{D}⟶{N}\right)\to {A}:{D}⟶{N}$
13 ffvelrn ${⊢}\left({A}:{D}⟶{N}\wedge {u}\in {D}\right)\to {A}\left({u}\right)\in {N}$
14 13 ad2ant2lr ${⊢}\left(\left({\phi }\wedge {A}:{D}⟶{N}\right)\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\right)\to {A}\left({u}\right)\in {N}$
15 14 adantr ${⊢}\left(\left(\left({\phi }\wedge {A}:{D}⟶{N}\right)\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\right)\wedge {A}\left({u}\right)={A}\left({w}\right)\right)\to {A}\left({u}\right)\in {N}$
16 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem1 ${⊢}{\phi }\to {X}\notin {N}$
17 preq1 ${⊢}{x}={u}\to \left\{{x},{y}\right\}=\left\{{u},{y}\right\}$
18 17 eleq1d ${⊢}{x}={u}\to \left(\left\{{x},{y}\right\}\in {E}↔\left\{{u},{y}\right\}\in {E}\right)$
19 18 riotabidv ${⊢}{x}={u}\to \left(\iota {y}\in {N}|\left\{{x},{y}\right\}\in {E}\right)=\left(\iota {y}\in {N}|\left\{{u},{y}\right\}\in {E}\right)$
20 19 cbvmptv ${⊢}\left({x}\in {D}⟼\left(\iota {y}\in {N}|\left\{{x},{y}\right\}\in {E}\right)\right)=\left({u}\in {D}⟼\left(\iota {y}\in {N}|\left\{{u},{y}\right\}\in {E}\right)\right)$
21 10 20 eqtri ${⊢}{A}=\left({u}\in {D}⟼\left(\iota {y}\in {N}|\left\{{u},{y}\right\}\in {E}\right)\right)$
22 1 2 3 4 5 6 7 8 9 21 frgrncvvdeqlem6 ${⊢}\left({\phi }\wedge {u}\in {D}\right)\to \left\{{u},{A}\left({u}\right)\right\}\in {E}$
23 preq1 ${⊢}{x}={w}\to \left\{{x},{y}\right\}=\left\{{w},{y}\right\}$
24 23 eleq1d ${⊢}{x}={w}\to \left(\left\{{x},{y}\right\}\in {E}↔\left\{{w},{y}\right\}\in {E}\right)$
25 24 riotabidv ${⊢}{x}={w}\to \left(\iota {y}\in {N}|\left\{{x},{y}\right\}\in {E}\right)=\left(\iota {y}\in {N}|\left\{{w},{y}\right\}\in {E}\right)$
26 25 cbvmptv ${⊢}\left({x}\in {D}⟼\left(\iota {y}\in {N}|\left\{{x},{y}\right\}\in {E}\right)\right)=\left({w}\in {D}⟼\left(\iota {y}\in {N}|\left\{{w},{y}\right\}\in {E}\right)\right)$
27 10 26 eqtri ${⊢}{A}=\left({w}\in {D}⟼\left(\iota {y}\in {N}|\left\{{w},{y}\right\}\in {E}\right)\right)$
28 1 2 3 4 5 6 7 8 9 27 frgrncvvdeqlem6 ${⊢}\left({\phi }\wedge {w}\in {D}\right)\to \left\{{w},{A}\left({w}\right)\right\}\in {E}$
29 22 28 anim12dan ${⊢}\left({\phi }\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\right)\to \left(\left\{{u},{A}\left({u}\right)\right\}\in {E}\wedge \left\{{w},{A}\left({w}\right)\right\}\in {E}\right)$
30 preq2 ${⊢}{A}\left({w}\right)={A}\left({u}\right)\to \left\{{w},{A}\left({w}\right)\right\}=\left\{{w},{A}\left({u}\right)\right\}$
31 30 eleq1d ${⊢}{A}\left({w}\right)={A}\left({u}\right)\to \left(\left\{{w},{A}\left({w}\right)\right\}\in {E}↔\left\{{w},{A}\left({u}\right)\right\}\in {E}\right)$
32 31 anbi2d ${⊢}{A}\left({w}\right)={A}\left({u}\right)\to \left(\left(\left\{{u},{A}\left({u}\right)\right\}\in {E}\wedge \left\{{w},{A}\left({w}\right)\right\}\in {E}\right)↔\left(\left\{{u},{A}\left({u}\right)\right\}\in {E}\wedge \left\{{w},{A}\left({u}\right)\right\}\in {E}\right)\right)$
33 32 eqcoms ${⊢}{A}\left({u}\right)={A}\left({w}\right)\to \left(\left(\left\{{u},{A}\left({u}\right)\right\}\in {E}\wedge \left\{{w},{A}\left({w}\right)\right\}\in {E}\right)↔\left(\left\{{u},{A}\left({u}\right)\right\}\in {E}\wedge \left\{{w},{A}\left({u}\right)\right\}\in {E}\right)\right)$
34 33 biimpa ${⊢}\left({A}\left({u}\right)={A}\left({w}\right)\wedge \left(\left\{{u},{A}\left({u}\right)\right\}\in {E}\wedge \left\{{w},{A}\left({w}\right)\right\}\in {E}\right)\right)\to \left(\left\{{u},{A}\left({u}\right)\right\}\in {E}\wedge \left\{{w},{A}\left({u}\right)\right\}\in {E}\right)$
35 df-ne ${⊢}{u}\ne {w}↔¬{u}={w}$
36 2 3 frgrnbnb ${⊢}\left({G}\in \mathrm{FriendGraph}\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\wedge {u}\ne {w}\right)\to \left(\left(\left\{{u},{A}\left({u}\right)\right\}\in {E}\wedge \left\{{w},{A}\left({u}\right)\right\}\in {E}\right)\to {A}\left({u}\right)={X}\right)$
37 9 36 syl3an1 ${⊢}\left({\phi }\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\wedge {u}\ne {w}\right)\to \left(\left(\left\{{u},{A}\left({u}\right)\right\}\in {E}\wedge \left\{{w},{A}\left({u}\right)\right\}\in {E}\right)\to {A}\left({u}\right)={X}\right)$
38 37 3expa ${⊢}\left(\left({\phi }\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\right)\wedge {u}\ne {w}\right)\to \left(\left(\left\{{u},{A}\left({u}\right)\right\}\in {E}\wedge \left\{{w},{A}\left({u}\right)\right\}\in {E}\right)\to {A}\left({u}\right)={X}\right)$
39 df-nel ${⊢}{X}\notin {N}↔¬{X}\in {N}$
40 eleq1 ${⊢}{A}\left({u}\right)={X}\to \left({A}\left({u}\right)\in {N}↔{X}\in {N}\right)$
41 40 biimpa ${⊢}\left({A}\left({u}\right)={X}\wedge {A}\left({u}\right)\in {N}\right)\to {X}\in {N}$
42 41 pm2.24d ${⊢}\left({A}\left({u}\right)={X}\wedge {A}\left({u}\right)\in {N}\right)\to \left(¬{X}\in {N}\to {u}={w}\right)$
43 42 expcom ${⊢}{A}\left({u}\right)\in {N}\to \left({A}\left({u}\right)={X}\to \left(¬{X}\in {N}\to {u}={w}\right)\right)$
44 43 com13 ${⊢}¬{X}\in {N}\to \left({A}\left({u}\right)={X}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)$
45 39 44 sylbi ${⊢}{X}\notin {N}\to \left({A}\left({u}\right)={X}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)$
46 45 com12 ${⊢}{A}\left({u}\right)={X}\to \left({X}\notin {N}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)$
47 38 46 syl6 ${⊢}\left(\left({\phi }\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\right)\wedge {u}\ne {w}\right)\to \left(\left(\left\{{u},{A}\left({u}\right)\right\}\in {E}\wedge \left\{{w},{A}\left({u}\right)\right\}\in {E}\right)\to \left({X}\notin {N}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)\right)$
48 47 expcom ${⊢}{u}\ne {w}\to \left(\left({\phi }\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\right)\to \left(\left(\left\{{u},{A}\left({u}\right)\right\}\in {E}\wedge \left\{{w},{A}\left({u}\right)\right\}\in {E}\right)\to \left({X}\notin {N}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)\right)\right)$
49 48 com23 ${⊢}{u}\ne {w}\to \left(\left(\left\{{u},{A}\left({u}\right)\right\}\in {E}\wedge \left\{{w},{A}\left({u}\right)\right\}\in {E}\right)\to \left(\left({\phi }\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\right)\to \left({X}\notin {N}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)\right)\right)$
50 35 49 sylbir ${⊢}¬{u}={w}\to \left(\left(\left\{{u},{A}\left({u}\right)\right\}\in {E}\wedge \left\{{w},{A}\left({u}\right)\right\}\in {E}\right)\to \left(\left({\phi }\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\right)\to \left({X}\notin {N}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)\right)\right)$
51 34 50 syl5com ${⊢}\left({A}\left({u}\right)={A}\left({w}\right)\wedge \left(\left\{{u},{A}\left({u}\right)\right\}\in {E}\wedge \left\{{w},{A}\left({w}\right)\right\}\in {E}\right)\right)\to \left(¬{u}={w}\to \left(\left({\phi }\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\right)\to \left({X}\notin {N}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)\right)\right)$
52 51 expcom ${⊢}\left(\left\{{u},{A}\left({u}\right)\right\}\in {E}\wedge \left\{{w},{A}\left({w}\right)\right\}\in {E}\right)\to \left({A}\left({u}\right)={A}\left({w}\right)\to \left(¬{u}={w}\to \left(\left({\phi }\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\right)\to \left({X}\notin {N}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)\right)\right)\right)$
53 52 com24 ${⊢}\left(\left\{{u},{A}\left({u}\right)\right\}\in {E}\wedge \left\{{w},{A}\left({w}\right)\right\}\in {E}\right)\to \left(\left({\phi }\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\right)\to \left(¬{u}={w}\to \left({A}\left({u}\right)={A}\left({w}\right)\to \left({X}\notin {N}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)\right)\right)\right)$
54 29 53 mpcom ${⊢}\left({\phi }\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\right)\to \left(¬{u}={w}\to \left({A}\left({u}\right)={A}\left({w}\right)\to \left({X}\notin {N}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)\right)\right)$
55 54 ex ${⊢}{\phi }\to \left(\left({u}\in {D}\wedge {w}\in {D}\right)\to \left(¬{u}={w}\to \left({A}\left({u}\right)={A}\left({w}\right)\to \left({X}\notin {N}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)\right)\right)\right)$
56 55 com3r ${⊢}¬{u}={w}\to \left({\phi }\to \left(\left({u}\in {D}\wedge {w}\in {D}\right)\to \left({A}\left({u}\right)={A}\left({w}\right)\to \left({X}\notin {N}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)\right)\right)\right)$
57 56 com15 ${⊢}{X}\notin {N}\to \left({\phi }\to \left(\left({u}\in {D}\wedge {w}\in {D}\right)\to \left({A}\left({u}\right)={A}\left({w}\right)\to \left(¬{u}={w}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)\right)\right)\right)$
58 16 57 mpcom ${⊢}{\phi }\to \left(\left({u}\in {D}\wedge {w}\in {D}\right)\to \left({A}\left({u}\right)={A}\left({w}\right)\to \left(¬{u}={w}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)\right)\right)$
59 58 expd ${⊢}{\phi }\to \left({u}\in {D}\to \left({w}\in {D}\to \left({A}\left({u}\right)={A}\left({w}\right)\to \left(¬{u}={w}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)\right)\right)\right)$
60 59 adantr ${⊢}\left({\phi }\wedge {A}:{D}⟶{N}\right)\to \left({u}\in {D}\to \left({w}\in {D}\to \left({A}\left({u}\right)={A}\left({w}\right)\to \left(¬{u}={w}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)\right)\right)\right)$
61 60 imp42 ${⊢}\left(\left(\left({\phi }\wedge {A}:{D}⟶{N}\right)\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\right)\wedge {A}\left({u}\right)={A}\left({w}\right)\right)\to \left(¬{u}={w}\to \left({A}\left({u}\right)\in {N}\to {u}={w}\right)\right)$
62 15 61 mpid ${⊢}\left(\left(\left({\phi }\wedge {A}:{D}⟶{N}\right)\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\right)\wedge {A}\left({u}\right)={A}\left({w}\right)\right)\to \left(¬{u}={w}\to {u}={w}\right)$
63 62 pm2.18d ${⊢}\left(\left(\left({\phi }\wedge {A}:{D}⟶{N}\right)\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\right)\wedge {A}\left({u}\right)={A}\left({w}\right)\right)\to {u}={w}$
64 63 ex ${⊢}\left(\left({\phi }\wedge {A}:{D}⟶{N}\right)\wedge \left({u}\in {D}\wedge {w}\in {D}\right)\right)\to \left({A}\left({u}\right)={A}\left({w}\right)\to {u}={w}\right)$
65 64 ralrimivva ${⊢}\left({\phi }\wedge {A}:{D}⟶{N}\right)\to \forall {u}\in {D}\phantom{\rule{.4em}{0ex}}\forall {w}\in {D}\phantom{\rule{.4em}{0ex}}\left({A}\left({u}\right)={A}\left({w}\right)\to {u}={w}\right)$
66 dff13 ${⊢}{A}:{D}\underset{1-1}{⟶}{N}↔\left({A}:{D}⟶{N}\wedge \forall {u}\in {D}\phantom{\rule{.4em}{0ex}}\forall {w}\in {D}\phantom{\rule{.4em}{0ex}}\left({A}\left({u}\right)={A}\left({w}\right)\to {u}={w}\right)\right)$
67 12 65 66 sylanbrc ${⊢}\left({\phi }\wedge {A}:{D}⟶{N}\right)\to {A}:{D}\underset{1-1}{⟶}{N}$
68 11 67 mpdan ${⊢}{\phi }\to {A}:{D}\underset{1-1}{⟶}{N}$