Metamath Proof Explorer

Theorem vtxduhgr0e

Description: The degree of a vertex in an empty hypergraph is zero, because there are no edges. Analogue of vtxdg0e . (Contributed by AV, 15-Dec-2020)

Ref Expression
Hypotheses vtxduhgr0e.v 
|- V = ( Vtx ` G )
vtxduhgr0e.e 
|- E = ( Edg ` G )
Assertion vtxduhgr0e 
|- ( ( G e. UHGraph /\ U e. V /\ E = (/) ) -> ( ( VtxDeg ` G ) ` U ) = 0 )

Proof

Step Hyp Ref Expression
1 vtxduhgr0e.v 
 |-  V = ( Vtx ` G )
2 vtxduhgr0e.e 
 |-  E = ( Edg ` G )
3 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
4 3 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
5 3 2 edg0iedg0 
 |-  ( Fun ( iEdg ` G ) -> ( E = (/) <-> ( iEdg ` G ) = (/) ) )
6 4 5 syl 
 |-  ( G e. UHGraph -> ( E = (/) <-> ( iEdg ` G ) = (/) ) )
7 6 adantr 
 |-  ( ( G e. UHGraph /\ U e. V ) -> ( E = (/) <-> ( iEdg ` G ) = (/) ) )
8 1 3 vtxdg0e 
 |-  ( ( U e. V /\ ( iEdg ` G ) = (/) ) -> ( ( VtxDeg ` G ) ` U ) = 0 )
9 8 ex 
 |-  ( U e. V -> ( ( iEdg ` G ) = (/) -> ( ( VtxDeg ` G ) ` U ) = 0 ) )
10 9 adantl 
 |-  ( ( G e. UHGraph /\ U e. V ) -> ( ( iEdg ` G ) = (/) -> ( ( VtxDeg ` G ) ` U ) = 0 ) )
11 7 10 sylbid 
 |-  ( ( G e. UHGraph /\ U e. V ) -> ( E = (/) -> ( ( VtxDeg ` G ) ` U ) = 0 ) )
12 11 3impia 
 |-  ( ( G e. UHGraph /\ U e. V /\ E = (/) ) -> ( ( VtxDeg ` G ) ` U ) = 0 )