Metamath Proof Explorer

Theorem uhgrnbgr0nb

Description: A vertex which is not endpoint of an edge has no neighbor in a hypergraph. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 26-Oct-2020)

Ref Expression
Assertion uhgrnbgr0nb ${⊢}\left({G}\in \mathrm{UHGraph}\wedge \forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{N}\notin {e}\right)\to {G}\mathrm{NeighbVtx}{N}=\varnothing$

Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
2 eqid ${⊢}\mathrm{Edg}\left({G}\right)=\mathrm{Edg}\left({G}\right)$
3 1 2 nbuhgr ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {N}\in \mathrm{V}\right)\to {G}\mathrm{NeighbVtx}{N}=\left\{{n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)|\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{N},{n}\right\}\subseteq {e}\right\}$
4 3 adantlr ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge \forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{N}\notin {e}\right)\wedge {N}\in \mathrm{V}\right)\to {G}\mathrm{NeighbVtx}{N}=\left\{{n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)|\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{N},{n}\right\}\subseteq {e}\right\}$
5 df-nel ${⊢}{N}\notin {e}↔¬{N}\in {e}$
6 prssg ${⊢}\left({N}\in \mathrm{V}\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)\right)\to \left(\left({N}\in {e}\wedge {n}\in {e}\right)↔\left\{{N},{n}\right\}\subseteq {e}\right)$
7 simpl ${⊢}\left({N}\in {e}\wedge {n}\in {e}\right)\to {N}\in {e}$
8 6 7 syl6bir ${⊢}\left({N}\in \mathrm{V}\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)\right)\to \left(\left\{{N},{n}\right\}\subseteq {e}\to {N}\in {e}\right)$
9 8 ad2antlr ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge \left({N}\in \mathrm{V}\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)\right)\right)\wedge {e}\in \mathrm{Edg}\left({G}\right)\right)\to \left(\left\{{N},{n}\right\}\subseteq {e}\to {N}\in {e}\right)$
10 9 con3d ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge \left({N}\in \mathrm{V}\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)\right)\right)\wedge {e}\in \mathrm{Edg}\left({G}\right)\right)\to \left(¬{N}\in {e}\to ¬\left\{{N},{n}\right\}\subseteq {e}\right)$
11 5 10 syl5bi ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge \left({N}\in \mathrm{V}\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)\right)\right)\wedge {e}\in \mathrm{Edg}\left({G}\right)\right)\to \left({N}\notin {e}\to ¬\left\{{N},{n}\right\}\subseteq {e}\right)$
12 11 ralimdva ${⊢}\left({G}\in \mathrm{UHGraph}\wedge \left({N}\in \mathrm{V}\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)\right)\right)\to \left(\forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{N}\notin {e}\to \forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}¬\left\{{N},{n}\right\}\subseteq {e}\right)$
13 12 imp ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge \left({N}\in \mathrm{V}\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)\right)\right)\wedge \forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{N}\notin {e}\right)\to \forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}¬\left\{{N},{n}\right\}\subseteq {e}$
14 ralnex ${⊢}\forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}¬\left\{{N},{n}\right\}\subseteq {e}↔¬\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{N},{n}\right\}\subseteq {e}$
15 13 14 sylib ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge \left({N}\in \mathrm{V}\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)\right)\right)\wedge \forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{N}\notin {e}\right)\to ¬\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{N},{n}\right\}\subseteq {e}$
16 15 expcom ${⊢}\forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{N}\notin {e}\to \left(\left({G}\in \mathrm{UHGraph}\wedge \left({N}\in \mathrm{V}\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)\right)\right)\to ¬\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{N},{n}\right\}\subseteq {e}\right)$
17 16 expd ${⊢}\forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{N}\notin {e}\to \left({G}\in \mathrm{UHGraph}\to \left(\left({N}\in \mathrm{V}\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)\right)\to ¬\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{N},{n}\right\}\subseteq {e}\right)\right)$
18 17 impcom ${⊢}\left({G}\in \mathrm{UHGraph}\wedge \forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{N}\notin {e}\right)\to \left(\left({N}\in \mathrm{V}\wedge {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)\right)\to ¬\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{N},{n}\right\}\subseteq {e}\right)$
19 18 expdimp ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge \forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{N}\notin {e}\right)\wedge {N}\in \mathrm{V}\right)\to \left({n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)\to ¬\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{N},{n}\right\}\subseteq {e}\right)$
20 19 ralrimiv ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge \forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{N}\notin {e}\right)\wedge {N}\in \mathrm{V}\right)\to \forall {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)\phantom{\rule{.4em}{0ex}}¬\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{N},{n}\right\}\subseteq {e}$
21 rabeq0 ${⊢}\left\{{n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)|\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{N},{n}\right\}\subseteq {e}\right\}=\varnothing ↔\forall {n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)\phantom{\rule{.4em}{0ex}}¬\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{N},{n}\right\}\subseteq {e}$
22 20 21 sylibr ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge \forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{N}\notin {e}\right)\wedge {N}\in \mathrm{V}\right)\to \left\{{n}\in \left(\mathrm{Vtx}\left({G}\right)\setminus \left\{{N}\right\}\right)|\exists {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left\{{N},{n}\right\}\subseteq {e}\right\}=\varnothing$
23 4 22 eqtrd ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge \forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{N}\notin {e}\right)\wedge {N}\in \mathrm{V}\right)\to {G}\mathrm{NeighbVtx}{N}=\varnothing$
24 23 expcom ${⊢}{N}\in \mathrm{V}\to \left(\left({G}\in \mathrm{UHGraph}\wedge \forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{N}\notin {e}\right)\to {G}\mathrm{NeighbVtx}{N}=\varnothing \right)$
25 id ${⊢}¬{N}\in \mathrm{V}\to ¬{N}\in \mathrm{V}$
26 25 intnand ${⊢}¬{N}\in \mathrm{V}\to ¬\left({G}\in \mathrm{V}\wedge {N}\in \mathrm{V}\right)$
27 nbgrprc0 ${⊢}¬\left({G}\in \mathrm{V}\wedge {N}\in \mathrm{V}\right)\to {G}\mathrm{NeighbVtx}{N}=\varnothing$
28 26 27 syl ${⊢}¬{N}\in \mathrm{V}\to {G}\mathrm{NeighbVtx}{N}=\varnothing$
29 28 a1d ${⊢}¬{N}\in \mathrm{V}\to \left(\left({G}\in \mathrm{UHGraph}\wedge \forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{N}\notin {e}\right)\to {G}\mathrm{NeighbVtx}{N}=\varnothing \right)$
30 24 29 pm2.61i ${⊢}\left({G}\in \mathrm{UHGraph}\wedge \forall {e}\in \mathrm{Edg}\left({G}\right)\phantom{\rule{.4em}{0ex}}{N}\notin {e}\right)\to {G}\mathrm{NeighbVtx}{N}=\varnothing$