Metamath Proof Explorer

Theorem vtxdumgrval

Description: The value of the vertex degree function for a multigraph. (Contributed by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 23-Feb-2021)

Ref Expression
Hypotheses vtxdlfgrval.v ⊢ V = Vtx ⁡ G
vtxdlfgrval.i ⊢ I = iEdg ⁡ G
vtxdlfgrval.a ⊢ A = dom ⁡ I
vtxdlfgrval.d ⊢ D = VtxDeg ⁡ G
Assertion vtxdumgrval ⊢ G ∈ UMGraph ∧ U ∈ V → D ⁡ U = x ∈ A | U ∈ I ⁡ x

Proof

Step Hyp Ref Expression
1 vtxdlfgrval.v ⊢ V = Vtx ⁡ G
2 vtxdlfgrval.i ⊢ I = iEdg ⁡ G
3 vtxdlfgrval.a ⊢ A = dom ⁡ I
4 vtxdlfgrval.d ⊢ D = VtxDeg ⁡ G
5 1 2 umgrislfupgr ⊢ G ∈ UMGraph ↔ G ∈ UPGraph ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x
6 3 eqcomi ⊢ dom ⁡ I = A
7 6 feq2i ⊢ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ↔ I : A ⟶ x ∈ 𝒫 V | 2 ≤ x
8 7 biimpi ⊢ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → I : A ⟶ x ∈ 𝒫 V | 2 ≤ x
9 5 8 simplbiim ⊢ G ∈ UMGraph → I : A ⟶ x ∈ 𝒫 V | 2 ≤ x
10 1 2 3 4 vtxdlfgrval ⊢ I : A ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ U ∈ V → D ⁡ U = x ∈ A | U ∈ I ⁡ x
11 9 10 sylan ⊢ G ∈ UMGraph ∧ U ∈ V → D ⁡ U = x ∈ A | U ∈ I ⁡ x