Metamath Proof Explorer

Theorem vtxdushgrfvedg

Description: The value of the vertex degree function for a simple hypergraph. (Contributed by AV, 12-Dec-2020) (Proof shortened by AV, 5-May-2021)

Ref Expression
Hypotheses vtxdushgrfvedg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
vtxdushgrfvedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
vtxdushgrfvedg.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion vtxdushgrfvedg ( ( 𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝐷 ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) +𝑒 ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑒 = { 𝑈 } } ) ) )

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 vtxdushgrfvedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 vtxdushgrfvedg.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
4 3 fveq1i ⊢ ( 𝐷 ‘ 𝑈 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 )
5 4 a1i ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝐷 ‘ 𝑈 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) )
6 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
7 eqid ⊢ dom ( iEdg ‘ 𝐺 ) = dom ( iEdg ‘ 𝐺 )
8 1 6 7 vtxdgval ⊢ ( 𝑈 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) } ) +𝑒 ( ♯ ‘ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝑈 } } ) ) )
9 8 adantl ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) } ) +𝑒 ( ♯ ‘ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝑈 } } ) ) )
10 1 2 vtxdushgrfvedglem ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) } ) = ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) )
11 fvex ⊢ ( iEdg ‘ 𝐺 ) ∈ V
12 11 dmex ⊢ dom ( iEdg ‘ 𝐺 ) ∈ V
13 12 rabex ⊢ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝑈 } } ∈ V
14 13 a1i ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉 ) → { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝑈 } } ∈ V )
15 eqid ⊢ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝑈 } } = { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝑈 } }
16 eqeq1 ⊢ ( 𝑒 = 𝑐 → ( 𝑒 = { 𝑈 } ↔ 𝑐 = { 𝑈 } ) )
17 16 cbvrabv ⊢ { 𝑒 ∈ 𝐸 ∣ 𝑒 = { 𝑈 } } = { 𝑐 ∈ 𝐸 ∣ 𝑐 = { 𝑈 } }
18 eqid ⊢ ( 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝑈 } } ↦ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝑈 } } ↦ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
19 2 6 15 17 18 ushgredgedgloop ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑥 ∈ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝑈 } } ↦ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) : { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝑈 } } –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑒 = { 𝑈 } } )
20 14 19 hasheqf1od ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝑈 } } ) = ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑒 = { 𝑈 } } ) )
21 10 20 oveq12d ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( ♯ ‘ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) } ) +𝑒 ( ♯ ‘ { 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝑈 } } ) ) = ( ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) +𝑒 ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑒 = { 𝑈 } } ) ) )
22 5 9 21 3eqtrd ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝐷 ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) +𝑒 ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑒 = { 𝑈 } } ) ) )