# Metamath Proof Explorer

## Theorem usgredg2v

Description: In a simple graph, the mapping of edges having a fixed endpoint to the other vertex of the edge is a one-to-one function into the set of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 18-Oct-2020)

Ref Expression
Hypotheses usgredg2v.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
usgredg2v.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
usgredg2v.a ${⊢}{A}=\left\{{x}\in \mathrm{dom}{E}|{N}\in {E}\left({x}\right)\right\}$
usgredg2v.f ${⊢}{F}=\left({y}\in {A}⟼\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)\right)$
Assertion usgredg2v ${⊢}\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\to {F}:{A}\underset{1-1}{⟶}{V}$

### Proof

Step Hyp Ref Expression
1 usgredg2v.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 usgredg2v.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
3 usgredg2v.a ${⊢}{A}=\left\{{x}\in \mathrm{dom}{E}|{N}\in {E}\left({x}\right)\right\}$
4 usgredg2v.f ${⊢}{F}=\left({y}\in {A}⟼\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)\right)$
5 1 2 3 usgredg2vlem1 ${⊢}\left({G}\in \mathrm{USGraph}\wedge {y}\in {A}\right)\to \left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)\in {V}$
6 5 ralrimiva ${⊢}{G}\in \mathrm{USGraph}\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)\in {V}$
7 6 adantr ${⊢}\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)\in {V}$
8 2 usgrf1 ${⊢}{G}\in \mathrm{USGraph}\to {E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}$
9 8 adantr ${⊢}\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\to {E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}$
10 elrabi ${⊢}{y}\in \left\{{x}\in \mathrm{dom}{E}|{N}\in {E}\left({x}\right)\right\}\to {y}\in \mathrm{dom}{E}$
11 10 3 eleq2s ${⊢}{y}\in {A}\to {y}\in \mathrm{dom}{E}$
12 elrabi ${⊢}{w}\in \left\{{x}\in \mathrm{dom}{E}|{N}\in {E}\left({x}\right)\right\}\to {w}\in \mathrm{dom}{E}$
13 12 3 eleq2s ${⊢}{w}\in {A}\to {w}\in \mathrm{dom}{E}$
14 11 13 anim12i ${⊢}\left({y}\in {A}\wedge {w}\in {A}\right)\to \left({y}\in \mathrm{dom}{E}\wedge {w}\in \mathrm{dom}{E}\right)$
15 f1fveq ${⊢}\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}\mathrm{ran}{E}\wedge \left({y}\in \mathrm{dom}{E}\wedge {w}\in \mathrm{dom}{E}\right)\right)\to \left({E}\left({y}\right)={E}\left({w}\right)↔{y}={w}\right)$
16 9 14 15 syl2an ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\wedge \left({y}\in {A}\wedge {w}\in {A}\right)\right)\to \left({E}\left({y}\right)={E}\left({w}\right)↔{y}={w}\right)$
17 16 bicomd ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\wedge \left({y}\in {A}\wedge {w}\in {A}\right)\right)\to \left({y}={w}↔{E}\left({y}\right)={E}\left({w}\right)\right)$
18 17 notbid ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\wedge \left({y}\in {A}\wedge {w}\in {A}\right)\right)\to \left(¬{y}={w}↔¬{E}\left({y}\right)={E}\left({w}\right)\right)$
19 simpl ${⊢}\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\to {G}\in \mathrm{USGraph}$
20 simpl ${⊢}\left({y}\in {A}\wedge {w}\in {A}\right)\to {y}\in {A}$
21 19 20 anim12i ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\wedge \left({y}\in {A}\wedge {w}\in {A}\right)\right)\to \left({G}\in \mathrm{USGraph}\wedge {y}\in {A}\right)$
22 preq1 ${⊢}{u}={z}\to \left\{{u},{N}\right\}=\left\{{z},{N}\right\}$
23 22 eqeq2d ${⊢}{u}={z}\to \left({E}\left({y}\right)=\left\{{u},{N}\right\}↔{E}\left({y}\right)=\left\{{z},{N}\right\}\right)$
24 23 cbvriotavw ${⊢}\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)$
25 1 2 3 usgredg2vlem2 ${⊢}\left({G}\in \mathrm{USGraph}\wedge {y}\in {A}\right)\to \left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)\to {E}\left({y}\right)=\left\{\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right),{N}\right\}\right)$
26 21 24 25 mpisyl ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\wedge \left({y}\in {A}\wedge {w}\in {A}\right)\right)\to {E}\left({y}\right)=\left\{\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right),{N}\right\}$
27 an3 ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\wedge \left({y}\in {A}\wedge {w}\in {A}\right)\right)\to \left({G}\in \mathrm{USGraph}\wedge {w}\in {A}\right)$
28 22 eqeq2d ${⊢}{u}={z}\to \left({E}\left({w}\right)=\left\{{u},{N}\right\}↔{E}\left({w}\right)=\left\{{z},{N}\right\}\right)$
29 28 cbvriotavw ${⊢}\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)$
30 1 2 3 usgredg2vlem2 ${⊢}\left({G}\in \mathrm{USGraph}\wedge {w}\in {A}\right)\to \left(\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)\to {E}\left({w}\right)=\left\{\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right),{N}\right\}\right)$
31 27 29 30 mpisyl ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\wedge \left({y}\in {A}\wedge {w}\in {A}\right)\right)\to {E}\left({w}\right)=\left\{\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right),{N}\right\}$
32 26 31 eqeq12d ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\wedge \left({y}\in {A}\wedge {w}\in {A}\right)\right)\to \left({E}\left({y}\right)={E}\left({w}\right)↔\left\{\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right),{N}\right\}=\left\{\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right),{N}\right\}\right)$
33 32 notbid ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\wedge \left({y}\in {A}\wedge {w}\in {A}\right)\right)\to \left(¬{E}\left({y}\right)={E}\left({w}\right)↔¬\left\{\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right),{N}\right\}=\left\{\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right),{N}\right\}\right)$
34 riotaex ${⊢}\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)\in \mathrm{V}$
35 34 a1i ${⊢}{N}\in {V}\to \left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)\in \mathrm{V}$
36 id ${⊢}{N}\in {V}\to {N}\in {V}$
37 riotaex ${⊢}\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\in \mathrm{V}$
38 37 a1i ${⊢}{N}\in {V}\to \left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\in \mathrm{V}$
39 preq12bg ${⊢}\left(\left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)\in \mathrm{V}\wedge {N}\in {V}\right)\wedge \left(\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\in \mathrm{V}\wedge {N}\in {V}\right)\right)\to \left(\left\{\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right),{N}\right\}=\left\{\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right),{N}\right\}↔\left(\left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\wedge {N}={N}\right)\vee \left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)={N}\wedge {N}=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\right)\right)\right)$
40 35 36 38 36 39 syl22anc ${⊢}{N}\in {V}\to \left(\left\{\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right),{N}\right\}=\left\{\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right),{N}\right\}↔\left(\left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\wedge {N}={N}\right)\vee \left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)={N}\wedge {N}=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\right)\right)\right)$
41 40 notbid ${⊢}{N}\in {V}\to \left(¬\left\{\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right),{N}\right\}=\left\{\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right),{N}\right\}↔¬\left(\left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\wedge {N}={N}\right)\vee \left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)={N}\wedge {N}=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\right)\right)\right)$
42 41 adantl ${⊢}\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\to \left(¬\left\{\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right),{N}\right\}=\left\{\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right),{N}\right\}↔¬\left(\left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\wedge {N}={N}\right)\vee \left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)={N}\wedge {N}=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\right)\right)\right)$
43 ioran ${⊢}¬\left(\left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\wedge {N}={N}\right)\vee \left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)={N}\wedge {N}=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\right)\right)↔\left(¬\left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\wedge {N}={N}\right)\wedge ¬\left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)={N}\wedge {N}=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\right)\right)$
44 ianor ${⊢}¬\left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\wedge {N}={N}\right)↔\left(¬\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\vee ¬{N}={N}\right)$
45 24 29 eqeq12i ${⊢}\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)↔\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)$
46 45 notbii ${⊢}¬\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)↔¬\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)$
47 46 biimpi ${⊢}¬\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\to ¬\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)$
48 47 a1d ${⊢}¬\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\to \left({G}\in \mathrm{USGraph}\to ¬\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)\right)$
49 eqid ${⊢}{N}={N}$
50 49 pm2.24i ${⊢}¬{N}={N}\to \left({G}\in \mathrm{USGraph}\to ¬\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)\right)$
51 48 50 jaoi ${⊢}\left(¬\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\vee ¬{N}={N}\right)\to \left({G}\in \mathrm{USGraph}\to ¬\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)\right)$
52 44 51 sylbi ${⊢}¬\left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\wedge {N}={N}\right)\to \left({G}\in \mathrm{USGraph}\to ¬\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)\right)$
53 52 adantr ${⊢}\left(¬\left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\wedge {N}={N}\right)\wedge ¬\left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)={N}\wedge {N}=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\right)\right)\to \left({G}\in \mathrm{USGraph}\to ¬\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)\right)$
54 43 53 sylbi ${⊢}¬\left(\left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\wedge {N}={N}\right)\vee \left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)={N}\wedge {N}=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\right)\right)\to \left({G}\in \mathrm{USGraph}\to ¬\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)\right)$
55 54 com12 ${⊢}{G}\in \mathrm{USGraph}\to \left(¬\left(\left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\wedge {N}={N}\right)\vee \left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)={N}\wedge {N}=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\right)\right)\to ¬\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)\right)$
56 55 adantr ${⊢}\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\to \left(¬\left(\left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\wedge {N}={N}\right)\vee \left(\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right)={N}\wedge {N}=\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right)\right)\right)\to ¬\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)\right)$
57 42 56 sylbid ${⊢}\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\to \left(¬\left\{\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right),{N}\right\}=\left\{\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right),{N}\right\}\to ¬\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)\right)$
58 57 adantr ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\wedge \left({y}\in {A}\wedge {w}\in {A}\right)\right)\to \left(¬\left\{\left(\iota {u}\in {V}|{E}\left({y}\right)=\left\{{u},{N}\right\}\right),{N}\right\}=\left\{\left(\iota {u}\in {V}|{E}\left({w}\right)=\left\{{u},{N}\right\}\right),{N}\right\}\to ¬\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)\right)$
59 33 58 sylbid ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\wedge \left({y}\in {A}\wedge {w}\in {A}\right)\right)\to \left(¬{E}\left({y}\right)={E}\left({w}\right)\to ¬\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)\right)$
60 18 59 sylbid ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\wedge \left({y}\in {A}\wedge {w}\in {A}\right)\right)\to \left(¬{y}={w}\to ¬\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)\right)$
61 60 con4d ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\wedge \left({y}\in {A}\wedge {w}\in {A}\right)\right)\to \left(\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)\to {y}={w}\right)$
62 61 ralrimivva ${⊢}\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)\to {y}={w}\right)$
63 fveqeq2 ${⊢}{y}={w}\to \left({E}\left({y}\right)=\left\{{z},{N}\right\}↔{E}\left({w}\right)=\left\{{z},{N}\right\}\right)$
64 63 riotabidv ${⊢}{y}={w}\to \left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)$
65 4 64 f1mpt ${⊢}{F}:{A}\underset{1-1}{⟶}{V}↔\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)\in {V}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left(\iota {z}\in {V}|{E}\left({y}\right)=\left\{{z},{N}\right\}\right)=\left(\iota {z}\in {V}|{E}\left({w}\right)=\left\{{z},{N}\right\}\right)\to {y}={w}\right)\right)$
66 7 62 65 sylanbrc ${⊢}\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\to {F}:{A}\underset{1-1}{⟶}{V}$