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 V U v 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 G U iEdg G i
6 5 adantl G UHGraph U V D U = 0 ¬ i dom iEdg G U iEdg G i
7 2 eleq2i U v E U v Edg G
8 4 uhgredgiedgb G UHGraph U v Edg G i dom iEdg G U v = iEdg G i
9 7 8 syl5bb G UHGraph U v E i dom iEdg G U v = iEdg G i
10 9 adantr G UHGraph U V U v E i dom iEdg G U v = iEdg G i
11 prid1g U V U U v
12 eleq2 U v = iEdg G i U U v U iEdg G i
13 11 12 syl5ibcom U V U v = iEdg G i U iEdg G i
14 13 adantl G UHGraph U V U v = iEdg G i U iEdg G i
15 14 reximdv G UHGraph U V i dom iEdg G U v = iEdg G i i dom iEdg G U iEdg G i
16 10 15 sylbid G UHGraph U V U v E i dom iEdg G U iEdg G i
17 16 rexlimdvw G UHGraph U V v V U v E i dom iEdg G U iEdg G i
18 17 con3d G UHGraph U V ¬ i dom iEdg G U iEdg G i ¬ v V U v E
19 6 18 sylbid G UHGraph U V D U = 0 ¬ v V U v E
20 19 3impia G UHGraph U V D U = 0 ¬ v V U v E