Metamath Proof Explorer


Theorem 1hevtxdg1

Description: The vertex degree of vertex D in a graph G with only one hyperedge E (not being a loop) is 1 if D is incident with the edge E . (Contributed by AV, 2-Mar-2021) (Proof shortened by AV, 17-Apr-2021)

Ref Expression
Hypotheses 1hevtxdg0.i φ iEdg G = A E
1hevtxdg0.v φ Vtx G = V
1hevtxdg0.a φ A X
1hevtxdg0.d φ D V
1hevtxdg1.e φ E 𝒫 V
1hevtxdg1.n φ D E
1hevtxdg1.l φ 2 E
Assertion 1hevtxdg1 φ VtxDeg G D = 1

Proof

Step Hyp Ref Expression
1 1hevtxdg0.i φ iEdg G = A E
2 1hevtxdg0.v φ Vtx G = V
3 1hevtxdg0.a φ A X
4 1hevtxdg0.d φ D V
5 1hevtxdg1.e φ E 𝒫 V
6 1hevtxdg1.n φ D E
7 1hevtxdg1.l φ 2 E
8 1 dmeqd φ dom iEdg G = dom A E
9 dmsnopg E 𝒫 V dom A E = A
10 5 9 syl φ dom A E = A
11 8 10 eqtrd φ dom iEdg G = A
12 fveq2 x = E x = E
13 12 breq2d x = E 2 x 2 E
14 2 pweqd φ 𝒫 Vtx G = 𝒫 V
15 5 14 eleqtrrd φ E 𝒫 Vtx G
16 13 15 7 elrabd φ E x 𝒫 Vtx G | 2 x
17 3 16 fsnd φ A E : A x 𝒫 Vtx G | 2 x
18 17 adantr φ dom iEdg G = A A E : A x 𝒫 Vtx G | 2 x
19 1 adantr φ dom iEdg G = A iEdg G = A E
20 simpr φ dom iEdg G = A dom iEdg G = A
21 19 20 feq12d φ dom iEdg G = A iEdg G : dom iEdg G x 𝒫 Vtx G | 2 x A E : A x 𝒫 Vtx G | 2 x
22 18 21 mpbird φ dom iEdg G = A iEdg G : dom iEdg G x 𝒫 Vtx G | 2 x
23 4 2 eleqtrrd φ D Vtx G
24 23 adantr φ dom iEdg G = A D Vtx G
25 eqid Vtx G = Vtx G
26 eqid iEdg G = iEdg G
27 eqid dom iEdg G = dom iEdg G
28 eqid VtxDeg G = VtxDeg G
29 25 26 27 28 vtxdlfgrval iEdg G : dom iEdg G x 𝒫 Vtx G | 2 x D Vtx G VtxDeg G D = x dom iEdg G | D iEdg G x
30 22 24 29 syl2anc φ dom iEdg G = A VtxDeg G D = x dom iEdg G | D iEdg G x
31 rabeq dom iEdg G = A x dom iEdg G | D iEdg G x = x A | D iEdg G x
32 31 adantl φ dom iEdg G = A x dom iEdg G | D iEdg G x = x A | D iEdg G x
33 32 fveq2d φ dom iEdg G = A x dom iEdg G | D iEdg G x = x A | D iEdg G x
34 fveq2 x = A iEdg G x = iEdg G A
35 34 eleq2d x = A D iEdg G x D iEdg G A
36 35 rabsnif x A | D iEdg G x = if D iEdg G A A
37 1 fveq1d φ iEdg G A = A E A
38 fvsng A X E 𝒫 V A E A = E
39 3 5 38 syl2anc φ A E A = E
40 37 39 eqtrd φ iEdg G A = E
41 6 40 eleqtrrd φ D iEdg G A
42 41 iftrued φ if D iEdg G A A = A
43 36 42 syl5eq φ x A | D iEdg G x = A
44 43 fveq2d φ x A | D iEdg G x = A
45 hashsng A X A = 1
46 3 45 syl φ A = 1
47 44 46 eqtrd φ x A | D iEdg G x = 1
48 47 adantr φ dom iEdg G = A x A | D iEdg G x = 1
49 30 33 48 3eqtrd φ dom iEdg G = A VtxDeg G D = 1
50 11 49 mpdan φ VtxDeg G D = 1