# Metamath Proof Explorer

## Theorem uhgr2edg

Description: If a vertex is adjacent to two different vertices in a hypergraph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 11-Feb-2021)

Ref Expression
Hypotheses usgrf1oedg.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
usgrf1oedg.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
uhgr2edg.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
Assertion uhgr2edg ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {N}\in {V}\right)\wedge \left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)\right)\to \exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\wedge {N}\in {I}\left({x}\right)\wedge {N}\in {I}\left({y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 usgrf1oedg.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
2 usgrf1oedg.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 uhgr2edg.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
4 simp1l ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {N}\in {V}\right)\wedge \left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)\right)\to {G}\in \mathrm{UHGraph}$
5 simp1r ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {N}\in {V}\right)\wedge \left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)\right)\to {A}\ne {B}$
6 simp23 ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {N}\in {V}\right)\wedge \left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)\right)\to {N}\in {V}$
7 simp21 ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {N}\in {V}\right)\wedge \left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)\right)\to {A}\in {V}$
8 3simpc ${⊢}\left({A}\in {V}\wedge {B}\in {V}\wedge {N}\in {V}\right)\to \left({B}\in {V}\wedge {N}\in {V}\right)$
9 8 3ad2ant2 ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {N}\in {V}\right)\wedge \left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)\right)\to \left({B}\in {V}\wedge {N}\in {V}\right)$
10 6 7 9 jca31 ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {N}\in {V}\right)\wedge \left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)\right)\to \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)$
11 4 5 10 jca31 ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {N}\in {V}\right)\wedge \left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)\right)\to \left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)$
12 simp3 ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {N}\in {V}\right)\wedge \left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)\right)\to \left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)$
13 2 a1i ${⊢}{G}\in \mathrm{UHGraph}\to {E}=\mathrm{Edg}\left({G}\right)$
14 edgval ${⊢}\mathrm{Edg}\left({G}\right)=\mathrm{ran}\mathrm{iEdg}\left({G}\right)$
15 14 a1i ${⊢}{G}\in \mathrm{UHGraph}\to \mathrm{Edg}\left({G}\right)=\mathrm{ran}\mathrm{iEdg}\left({G}\right)$
16 1 eqcomi ${⊢}\mathrm{iEdg}\left({G}\right)={I}$
17 16 a1i ${⊢}{G}\in \mathrm{UHGraph}\to \mathrm{iEdg}\left({G}\right)={I}$
18 17 rneqd ${⊢}{G}\in \mathrm{UHGraph}\to \mathrm{ran}\mathrm{iEdg}\left({G}\right)=\mathrm{ran}{I}$
19 13 15 18 3eqtrd ${⊢}{G}\in \mathrm{UHGraph}\to {E}=\mathrm{ran}{I}$
20 19 eleq2d ${⊢}{G}\in \mathrm{UHGraph}\to \left(\left\{{N},{A}\right\}\in {E}↔\left\{{N},{A}\right\}\in \mathrm{ran}{I}\right)$
21 19 eleq2d ${⊢}{G}\in \mathrm{UHGraph}\to \left(\left\{{B},{N}\right\}\in {E}↔\left\{{B},{N}\right\}\in \mathrm{ran}{I}\right)$
22 20 21 anbi12d ${⊢}{G}\in \mathrm{UHGraph}\to \left(\left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)↔\left(\left\{{N},{A}\right\}\in \mathrm{ran}{I}\wedge \left\{{B},{N}\right\}\in \mathrm{ran}{I}\right)\right)$
23 1 uhgrfun ${⊢}{G}\in \mathrm{UHGraph}\to \mathrm{Fun}{I}$
24 23 funfnd ${⊢}{G}\in \mathrm{UHGraph}\to {I}Fn\mathrm{dom}{I}$
25 fvelrnb ${⊢}{I}Fn\mathrm{dom}{I}\to \left(\left\{{N},{A}\right\}\in \mathrm{ran}{I}↔\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)=\left\{{N},{A}\right\}\right)$
26 fvelrnb ${⊢}{I}Fn\mathrm{dom}{I}\to \left(\left\{{B},{N}\right\}\in \mathrm{ran}{I}↔\exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({y}\right)=\left\{{B},{N}\right\}\right)$
27 25 26 anbi12d ${⊢}{I}Fn\mathrm{dom}{I}\to \left(\left(\left\{{N},{A}\right\}\in \mathrm{ran}{I}\wedge \left\{{B},{N}\right\}\in \mathrm{ran}{I}\right)↔\left(\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)=\left\{{N},{A}\right\}\wedge \exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({y}\right)=\left\{{B},{N}\right\}\right)\right)$
28 24 27 syl ${⊢}{G}\in \mathrm{UHGraph}\to \left(\left(\left\{{N},{A}\right\}\in \mathrm{ran}{I}\wedge \left\{{B},{N}\right\}\in \mathrm{ran}{I}\right)↔\left(\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)=\left\{{N},{A}\right\}\wedge \exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({y}\right)=\left\{{B},{N}\right\}\right)\right)$
29 22 28 bitrd ${⊢}{G}\in \mathrm{UHGraph}\to \left(\left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)↔\left(\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)=\left\{{N},{A}\right\}\wedge \exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({y}\right)=\left\{{B},{N}\right\}\right)\right)$
30 29 ad2antrr ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\to \left(\left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)↔\left(\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)=\left\{{N},{A}\right\}\wedge \exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({y}\right)=\left\{{B},{N}\right\}\right)\right)$
31 reeanv ${⊢}\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\left({I}\left({x}\right)=\left\{{N},{A}\right\}\wedge {I}\left({y}\right)=\left\{{B},{N}\right\}\right)↔\left(\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)=\left\{{N},{A}\right\}\wedge \exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({y}\right)=\left\{{B},{N}\right\}\right)$
32 fveqeq2 ${⊢}{x}={y}\to \left({I}\left({x}\right)=\left\{{N},{A}\right\}↔{I}\left({y}\right)=\left\{{N},{A}\right\}\right)$
33 32 anbi1d ${⊢}{x}={y}\to \left(\left({I}\left({x}\right)=\left\{{N},{A}\right\}\wedge {I}\left({y}\right)=\left\{{B},{N}\right\}\right)↔\left({I}\left({y}\right)=\left\{{N},{A}\right\}\wedge {I}\left({y}\right)=\left\{{B},{N}\right\}\right)\right)$
34 eqtr2 ${⊢}\left({I}\left({y}\right)=\left\{{N},{A}\right\}\wedge {I}\left({y}\right)=\left\{{B},{N}\right\}\right)\to \left\{{N},{A}\right\}=\left\{{B},{N}\right\}$
35 prcom ${⊢}\left\{{B},{N}\right\}=\left\{{N},{B}\right\}$
36 35 eqeq2i ${⊢}\left\{{N},{A}\right\}=\left\{{B},{N}\right\}↔\left\{{N},{A}\right\}=\left\{{N},{B}\right\}$
37 preq12bg ${⊢}\left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({N}\in {V}\wedge {B}\in {V}\right)\right)\to \left(\left\{{N},{A}\right\}=\left\{{N},{B}\right\}↔\left(\left({N}={N}\wedge {A}={B}\right)\vee \left({N}={B}\wedge {A}={N}\right)\right)\right)$
38 37 ancom2s ${⊢}\left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\to \left(\left\{{N},{A}\right\}=\left\{{N},{B}\right\}↔\left(\left({N}={N}\wedge {A}={B}\right)\vee \left({N}={B}\wedge {A}={N}\right)\right)\right)$
39 eqneqall ${⊢}{A}={B}\to \left({A}\ne {B}\to {x}\ne {y}\right)$
40 39 adantl ${⊢}\left({N}={N}\wedge {A}={B}\right)\to \left({A}\ne {B}\to {x}\ne {y}\right)$
41 eqtr ${⊢}\left({A}={N}\wedge {N}={B}\right)\to {A}={B}$
42 41 ancoms ${⊢}\left({N}={B}\wedge {A}={N}\right)\to {A}={B}$
43 42 39 syl ${⊢}\left({N}={B}\wedge {A}={N}\right)\to \left({A}\ne {B}\to {x}\ne {y}\right)$
44 40 43 jaoi ${⊢}\left(\left({N}={N}\wedge {A}={B}\right)\vee \left({N}={B}\wedge {A}={N}\right)\right)\to \left({A}\ne {B}\to {x}\ne {y}\right)$
45 44 adantld ${⊢}\left(\left({N}={N}\wedge {A}={B}\right)\vee \left({N}={B}\wedge {A}={N}\right)\right)\to \left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\to {x}\ne {y}\right)$
46 38 45 syl6bi ${⊢}\left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\to \left(\left\{{N},{A}\right\}=\left\{{N},{B}\right\}\to \left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\to {x}\ne {y}\right)\right)$
47 46 com3l ${⊢}\left\{{N},{A}\right\}=\left\{{N},{B}\right\}\to \left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\to \left(\left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\to {x}\ne {y}\right)\right)$
48 47 impd ${⊢}\left\{{N},{A}\right\}=\left\{{N},{B}\right\}\to \left(\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\to {x}\ne {y}\right)$
49 36 48 sylbi ${⊢}\left\{{N},{A}\right\}=\left\{{B},{N}\right\}\to \left(\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\to {x}\ne {y}\right)$
50 34 49 syl ${⊢}\left({I}\left({y}\right)=\left\{{N},{A}\right\}\wedge {I}\left({y}\right)=\left\{{B},{N}\right\}\right)\to \left(\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\to {x}\ne {y}\right)$
51 33 50 syl6bi ${⊢}{x}={y}\to \left(\left({I}\left({x}\right)=\left\{{N},{A}\right\}\wedge {I}\left({y}\right)=\left\{{B},{N}\right\}\right)\to \left(\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\to {x}\ne {y}\right)\right)$
52 51 impcomd ${⊢}{x}={y}\to \left(\left(\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\wedge \left({I}\left({x}\right)=\left\{{N},{A}\right\}\wedge {I}\left({y}\right)=\left\{{B},{N}\right\}\right)\right)\to {x}\ne {y}\right)$
53 ax-1 ${⊢}{x}\ne {y}\to \left(\left(\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\wedge \left({I}\left({x}\right)=\left\{{N},{A}\right\}\wedge {I}\left({y}\right)=\left\{{B},{N}\right\}\right)\right)\to {x}\ne {y}\right)$
54 52 53 pm2.61ine ${⊢}\left(\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\wedge \left({I}\left({x}\right)=\left\{{N},{A}\right\}\wedge {I}\left({y}\right)=\left\{{B},{N}\right\}\right)\right)\to {x}\ne {y}$
55 prid1g ${⊢}{N}\in {V}\to {N}\in \left\{{N},{A}\right\}$
56 55 ad2antrr ${⊢}\left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\to {N}\in \left\{{N},{A}\right\}$
57 56 adantl ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\to {N}\in \left\{{N},{A}\right\}$
58 eleq2 ${⊢}{I}\left({x}\right)=\left\{{N},{A}\right\}\to \left({N}\in {I}\left({x}\right)↔{N}\in \left\{{N},{A}\right\}\right)$
59 57 58 syl5ibr ${⊢}{I}\left({x}\right)=\left\{{N},{A}\right\}\to \left(\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\to {N}\in {I}\left({x}\right)\right)$
60 59 adantr ${⊢}\left({I}\left({x}\right)=\left\{{N},{A}\right\}\wedge {I}\left({y}\right)=\left\{{B},{N}\right\}\right)\to \left(\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\to {N}\in {I}\left({x}\right)\right)$
61 60 impcom ${⊢}\left(\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\wedge \left({I}\left({x}\right)=\left\{{N},{A}\right\}\wedge {I}\left({y}\right)=\left\{{B},{N}\right\}\right)\right)\to {N}\in {I}\left({x}\right)$
62 prid2g ${⊢}{N}\in {V}\to {N}\in \left\{{B},{N}\right\}$
63 62 ad2antrr ${⊢}\left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\to {N}\in \left\{{B},{N}\right\}$
64 63 adantl ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\to {N}\in \left\{{B},{N}\right\}$
65 eleq2 ${⊢}{I}\left({y}\right)=\left\{{B},{N}\right\}\to \left({N}\in {I}\left({y}\right)↔{N}\in \left\{{B},{N}\right\}\right)$
66 64 65 syl5ibr ${⊢}{I}\left({y}\right)=\left\{{B},{N}\right\}\to \left(\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\to {N}\in {I}\left({y}\right)\right)$
67 66 adantl ${⊢}\left({I}\left({x}\right)=\left\{{N},{A}\right\}\wedge {I}\left({y}\right)=\left\{{B},{N}\right\}\right)\to \left(\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\to {N}\in {I}\left({y}\right)\right)$
68 67 impcom ${⊢}\left(\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\wedge \left({I}\left({x}\right)=\left\{{N},{A}\right\}\wedge {I}\left({y}\right)=\left\{{B},{N}\right\}\right)\right)\to {N}\in {I}\left({y}\right)$
69 54 61 68 3jca ${⊢}\left(\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\wedge \left({I}\left({x}\right)=\left\{{N},{A}\right\}\wedge {I}\left({y}\right)=\left\{{B},{N}\right\}\right)\right)\to \left({x}\ne {y}\wedge {N}\in {I}\left({x}\right)\wedge {N}\in {I}\left({y}\right)\right)$
70 69 ex ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\to \left(\left({I}\left({x}\right)=\left\{{N},{A}\right\}\wedge {I}\left({y}\right)=\left\{{B},{N}\right\}\right)\to \left({x}\ne {y}\wedge {N}\in {I}\left({x}\right)\wedge {N}\in {I}\left({y}\right)\right)\right)$
71 70 reximdv ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\to \left(\exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\left({I}\left({x}\right)=\left\{{N},{A}\right\}\wedge {I}\left({y}\right)=\left\{{B},{N}\right\}\right)\to \exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\wedge {N}\in {I}\left({x}\right)\wedge {N}\in {I}\left({y}\right)\right)\right)$
72 71 reximdv ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\to \left(\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\left({I}\left({x}\right)=\left\{{N},{A}\right\}\wedge {I}\left({y}\right)=\left\{{B},{N}\right\}\right)\to \exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\wedge {N}\in {I}\left({x}\right)\wedge {N}\in {I}\left({y}\right)\right)\right)$
73 31 72 syl5bir ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\to \left(\left(\exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)=\left\{{N},{A}\right\}\wedge \exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}{I}\left({y}\right)=\left\{{B},{N}\right\}\right)\to \exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\wedge {N}\in {I}\left({x}\right)\wedge {N}\in {I}\left({y}\right)\right)\right)$
74 30 73 sylbid ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left(\left({N}\in {V}\wedge {A}\in {V}\right)\wedge \left({B}\in {V}\wedge {N}\in {V}\right)\right)\right)\to \left(\left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)\to \exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\wedge {N}\in {I}\left({x}\right)\wedge {N}\in {I}\left({y}\right)\right)\right)$
75 11 12 74 sylc ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {A}\ne {B}\right)\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {N}\in {V}\right)\wedge \left(\left\{{N},{A}\right\}\in {E}\wedge \left\{{B},{N}\right\}\in {E}\right)\right)\to \exists {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\wedge {N}\in {I}\left({x}\right)\wedge {N}\in {I}\left({y}\right)\right)$