Metamath Proof Explorer

Theorem 1hevtxdg0

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

Ref Expression
Hypotheses 1hevtxdg0.i ⊢ φ → iEdg ⁡ G = A E
1hevtxdg0.v ⊢ φ → Vtx ⁡ G = V
1hevtxdg0.a ⊢ φ → A ∈ X
1hevtxdg0.d ⊢ φ → D ∈ V
1hevtxdg0.e ⊢ φ → E ∈ Y
1hevtxdg0.n ⊢ φ → D ∉ E
Assertion 1hevtxdg0 ⊢ φ → VtxDeg ⁡ G ⁡ D = 0

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 1hevtxdg0.e ⊢ φ → E ∈ Y
6 1hevtxdg0.n ⊢ φ → D ∉ E
7 df-nel ⊢ D ∉ E ↔ ¬ D ∈ E
8 6 7 sylib ⊢ φ → ¬ D ∈ E
9 1 fveq1d ⊢ φ → iEdg ⁡ G ⁡ A = A E ⁡ A
10 fvsng ⊢ A ∈ X ∧ E ∈ Y → A E ⁡ A = E
11 3 5 10 syl2anc ⊢ φ → A E ⁡ A = E
12 9 11 eqtrd ⊢ φ → iEdg ⁡ G ⁡ A = E
13 8 12 neleqtrrd ⊢ φ → ¬ D ∈ iEdg ⁡ G ⁡ A
14 fveq2 ⊢ x = A → iEdg ⁡ G ⁡ x = iEdg ⁡ G ⁡ A
15 14 eleq2d ⊢ x = A → D ∈ iEdg ⁡ G ⁡ x ↔ D ∈ iEdg ⁡ G ⁡ A
16 15 notbid ⊢ x = A → ¬ D ∈ iEdg ⁡ G ⁡ x ↔ ¬ D ∈ iEdg ⁡ G ⁡ A
17 16 ralsng ⊢ A ∈ X → ∀ x ∈ A ¬ D ∈ iEdg ⁡ G ⁡ x ↔ ¬ D ∈ iEdg ⁡ G ⁡ A
18 3 17 syl ⊢ φ → ∀ x ∈ A ¬ D ∈ iEdg ⁡ G ⁡ x ↔ ¬ D ∈ iEdg ⁡ G ⁡ A
19 13 18 mpbird ⊢ φ → ∀ x ∈ A ¬ D ∈ iEdg ⁡ G ⁡ x
20 1 dmeqd ⊢ φ → dom ⁡ iEdg ⁡ G = dom ⁡ A E
21 dmsnopg ⊢ E ∈ Y → dom ⁡ A E = A
22 5 21 syl ⊢ φ → dom ⁡ A E = A
23 20 22 eqtrd ⊢ φ → dom ⁡ iEdg ⁡ G = A
24 19 23 raleqtrrdv ⊢ φ → ∀ x ∈ dom ⁡ iEdg ⁡ G ¬ D ∈ iEdg ⁡ G ⁡ x
25 ralnex ⊢ ∀ x ∈ dom ⁡ iEdg ⁡ G ¬ D ∈ iEdg ⁡ G ⁡ x ↔ ¬ ∃ x ∈ dom ⁡ iEdg ⁡ G D ∈ iEdg ⁡ G ⁡ x
26 24 25 sylib ⊢ φ → ¬ ∃ x ∈ dom ⁡ iEdg ⁡ G D ∈ iEdg ⁡ G ⁡ x
27 2 eleq2d ⊢ φ → D ∈ Vtx ⁡ G ↔ D ∈ V
28 4 27 mpbird ⊢ φ → D ∈ Vtx ⁡ G
29 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
30 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
31 eqid ⊢ VtxDeg ⁡ G = VtxDeg ⁡ G
32 29 30 31 vtxd0nedgb ⊢ D ∈ Vtx ⁡ G → VtxDeg ⁡ G ⁡ D = 0 ↔ ¬ ∃ x ∈ dom ⁡ iEdg ⁡ G D ∈ iEdg ⁡ G ⁡ x
33 28 32 syl ⊢ φ → VtxDeg ⁡ G ⁡ D = 0 ↔ ¬ ∃ x ∈ dom ⁡ iEdg ⁡ G D ∈ iEdg ⁡ G ⁡ x
34 26 33 mpbird ⊢ φ → VtxDeg ⁡ G ⁡ D = 0