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 eqtrid ⊢ φ → 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