Metamath Proof Explorer


Theorem vtxduhgr0edgnel

Description: A vertex in a hypergraph has degree 0 iff there is no edge incident with this vertex. (Contributed by AV, 24-Dec-2020)

Ref Expression
Hypotheses vtxdushgrfvedg.v 𝑉 = ( Vtx ‘ 𝐺 )
vtxdushgrfvedg.e 𝐸 = ( Edg ‘ 𝐺 )
vtxdushgrfvedg.d 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion vtxduhgr0edgnel ( ( 𝐺 ∈ UHGraph ∧ 𝑈𝑉 ) → ( ( 𝐷𝑈 ) = 0 ↔ ¬ ∃ 𝑒𝐸 𝑈𝑒 ) )

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v 𝑉 = ( Vtx ‘ 𝐺 )
2 vtxdushgrfvedg.e 𝐸 = ( Edg ‘ 𝐺 )
3 vtxdushgrfvedg.d 𝐷 = ( VtxDeg ‘ 𝐺 )
4 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
5 1 4 3 vtxd0nedgb ( 𝑈𝑉 → ( ( 𝐷𝑈 ) = 0 ↔ ¬ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
6 5 adantl ( ( 𝐺 ∈ UHGraph ∧ 𝑈𝑉 ) → ( ( 𝐷𝑈 ) = 0 ↔ ¬ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
7 4 2 uhgrvtxedgiedgb ( ( 𝐺 ∈ UHGraph ∧ 𝑈𝑉 ) → ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ↔ ∃ 𝑒𝐸 𝑈𝑒 ) )
8 7 notbid ( ( 𝐺 ∈ UHGraph ∧ 𝑈𝑉 ) → ( ¬ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ↔ ¬ ∃ 𝑒𝐸 𝑈𝑒 ) )
9 6 8 bitrd ( ( 𝐺 ∈ UHGraph ∧ 𝑈𝑉 ) → ( ( 𝐷𝑈 ) = 0 ↔ ¬ ∃ 𝑒𝐸 𝑈𝑒 ) )