This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ↔ ¬ ∃ 𝑒 ∈ 𝐸 𝑈 ∈ 𝑒 ) )