Metamath Proof Explorer

Theorem vtxduhgr0nedg

Description: If a vertex in a hypergraph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017) (Revised by AV, 15-Dec-2020) (Proof shortened by AV, 24-Dec-2020)

Ref Expression
Hypotheses vtxdushgrfvedg.v ⊢V=Vtx⁡G
vtxdushgrfvedg.e ⊢E=Edg⁡G
vtxdushgrfvedg.d ⊢D=VtxDeg⁡G
Assertion vtxduhgr0nedg ⊢G∈UHGraph∧U∈V∧D⁡U=0→¬∃v∈VUv∈E

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v ⊢V=Vtx⁡G
2 vtxdushgrfvedg.e ⊢E=Edg⁡G
3 vtxdushgrfvedg.d ⊢D=VtxDeg⁡G
4 eqid ⊢iEdg⁡G=iEdg⁡G
5 1 4 3 vtxd0nedgb ⊢U∈V→D⁡U=0↔¬∃i∈dom⁡iEdg⁡GU∈iEdg⁡G⁡i
6 5 adantl ⊢G∈UHGraph∧U∈V→D⁡U=0↔¬∃i∈dom⁡iEdg⁡GU∈iEdg⁡G⁡i
7 2 eleq2i ⊢Uv∈E↔Uv∈Edg⁡G
8 4 uhgredgiedgb ⊢G∈UHGraph→Uv∈Edg⁡G↔∃i∈dom⁡iEdg⁡GUv=iEdg⁡G⁡i
9 7 8 syl5bb ⊢G∈UHGraph→Uv∈E↔∃i∈dom⁡iEdg⁡GUv=iEdg⁡G⁡i
10 9 adantr ⊢G∈UHGraph∧U∈V→Uv∈E↔∃i∈dom⁡iEdg⁡GUv=iEdg⁡G⁡i
11 prid1g ⊢U∈V→U∈Uv
12 eleq2 ⊢Uv=iEdg⁡G⁡i→U∈Uv↔U∈iEdg⁡G⁡i
13 11 12 syl5ibcom ⊢U∈V→Uv=iEdg⁡G⁡i→U∈iEdg⁡G⁡i
14 13 adantl ⊢G∈UHGraph∧U∈V→Uv=iEdg⁡G⁡i→U∈iEdg⁡G⁡i
15 14 reximdv ⊢G∈UHGraph∧U∈V→∃i∈dom⁡iEdg⁡GUv=iEdg⁡G⁡i→∃i∈dom⁡iEdg⁡GU∈iEdg⁡G⁡i
16 10 15 sylbid ⊢G∈UHGraph∧U∈V→Uv∈E→∃i∈dom⁡iEdg⁡GU∈iEdg⁡G⁡i
17 16 rexlimdvw ⊢G∈UHGraph∧U∈V→∃v∈VUv∈E→∃i∈dom⁡iEdg⁡GU∈iEdg⁡G⁡i
18 17 con3d ⊢G∈UHGraph∧U∈V→¬∃i∈dom⁡iEdg⁡GU∈iEdg⁡G⁡i→¬∃v∈VUv∈E
19 6 18 sylbid ⊢G∈UHGraph∧U∈V→D⁡U=0→¬∃v∈VUv∈E
20 19 3impia ⊢G∈UHGraph∧U∈V∧D⁡U=0→¬∃v∈VUv∈E