Metamath Proof Explorer


Theorem vtxd0nedgb

Description: A vertex has degree 0 iff there is no edge incident with the vertex. (Contributed by AV, 24-Dec-2020) (Revised by AV, 22-Mar-2021)

Ref Expression
Hypotheses vtxd0nedgb.v V = Vtx G
vtxd0nedgb.i I = iEdg G
vtxd0nedgb.d D = VtxDeg G
Assertion vtxd0nedgb U V D U = 0 ¬ i dom I U I i

Proof

Step Hyp Ref Expression
1 vtxd0nedgb.v V = Vtx G
2 vtxd0nedgb.i I = iEdg G
3 vtxd0nedgb.d D = VtxDeg G
4 3 fveq1i D U = VtxDeg G U
5 eqid dom I = dom I
6 1 2 5 vtxdgval U V VtxDeg G U = i dom I | U I i + 𝑒 i dom I | I i = U
7 4 6 syl5eq U V D U = i dom I | U I i + 𝑒 i dom I | I i = U
8 7 eqeq1d U V D U = 0 i dom I | U I i + 𝑒 i dom I | I i = U = 0
9 2 fvexi I V
10 9 dmex dom I V
11 10 rabex i dom I | U I i V
12 hashxnn0 i dom I | U I i V i dom I | U I i 0 *
13 11 12 ax-mp i dom I | U I i 0 *
14 10 rabex i dom I | I i = U V
15 hashxnn0 i dom I | I i = U V i dom I | I i = U 0 *
16 14 15 ax-mp i dom I | I i = U 0 *
17 13 16 pm3.2i i dom I | U I i 0 * i dom I | I i = U 0 *
18 xnn0xadd0 i dom I | U I i 0 * i dom I | I i = U 0 * i dom I | U I i + 𝑒 i dom I | I i = U = 0 i dom I | U I i = 0 i dom I | I i = U = 0
19 17 18 mp1i U V i dom I | U I i + 𝑒 i dom I | I i = U = 0 i dom I | U I i = 0 i dom I | I i = U = 0
20 hasheq0 i dom I | U I i V i dom I | U I i = 0 i dom I | U I i =
21 11 20 ax-mp i dom I | U I i = 0 i dom I | U I i =
22 hasheq0 i dom I | I i = U V i dom I | I i = U = 0 i dom I | I i = U =
23 14 22 ax-mp i dom I | I i = U = 0 i dom I | I i = U =
24 21 23 anbi12i i dom I | U I i = 0 i dom I | I i = U = 0 i dom I | U I i = i dom I | I i = U =
25 rabeq0 i dom I | U I i = i dom I ¬ U I i
26 rabeq0 i dom I | I i = U = i dom I ¬ I i = U
27 25 26 anbi12i i dom I | U I i = i dom I | I i = U = i dom I ¬ U I i i dom I ¬ I i = U
28 ralnex i dom I ¬ U I i I i = U ¬ i dom I U I i I i = U
29 28 bicomi ¬ i dom I U I i I i = U i dom I ¬ U I i I i = U
30 ioran ¬ U I i I i = U ¬ U I i ¬ I i = U
31 30 ralbii i dom I ¬ U I i I i = U i dom I ¬ U I i ¬ I i = U
32 r19.26 i dom I ¬ U I i ¬ I i = U i dom I ¬ U I i i dom I ¬ I i = U
33 29 31 32 3bitri ¬ i dom I U I i I i = U i dom I ¬ U I i i dom I ¬ I i = U
34 33 bicomi i dom I ¬ U I i i dom I ¬ I i = U ¬ i dom I U I i I i = U
35 24 27 34 3bitri i dom I | U I i = 0 i dom I | I i = U = 0 ¬ i dom I U I i I i = U
36 orcom U I i I i = U I i = U U I i
37 snidg U V U U
38 eleq2 I i = U U I i U U
39 37 38 syl5ibrcom U V I i = U U I i
40 pm4.72 I i = U U I i U I i I i = U U I i
41 39 40 sylib U V U I i I i = U U I i
42 36 41 bitr4id U V U I i I i = U U I i
43 42 rexbidv U V i dom I U I i I i = U i dom I U I i
44 43 notbid U V ¬ i dom I U I i I i = U ¬ i dom I U I i
45 35 44 syl5bb U V i dom I | U I i = 0 i dom I | I i = U = 0 ¬ i dom I U I i
46 8 19 45 3bitrd U V D U = 0 ¬ i dom I U I i