Metamath Proof Explorer

Theorem vtxdlfuhgr1v

Description: The degree of the vertex in a loop-free hypergraph with one vertex is 0. (Contributed by AV, 2-Apr-2021)

Ref Expression
Hypotheses vtxdlfuhgr1v.v 
|- V = ( Vtx ` G )
vtxdlfuhgr1v.i 
|- I = ( iEdg ` G )
vtxdlfuhgr1v.e 
|- E = { x e. ~P V | 2 <_ ( # ` x ) }
Assertion vtxdlfuhgr1v 
|- ( ( G e. UHGraph /\ ( # ` V ) = 1 /\ I : dom I --> E ) -> ( U e. V -> ( ( VtxDeg ` G ) ` U ) = 0 ) )

Proof

Step Hyp Ref Expression
1 vtxdlfuhgr1v.v 
 |-  V = ( Vtx ` G )
2 vtxdlfuhgr1v.i 
 |-  I = ( iEdg ` G )
3 vtxdlfuhgr1v.e 
 |-  E = { x e. ~P V | 2 <_ ( # ` x ) }
4 simpl1 
 |-  ( ( ( G e. UHGraph /\ ( # ` V ) = 1 /\ I : dom I --> E ) /\ U e. V ) -> G e. UHGraph )
5 simpr 
 |-  ( ( ( G e. UHGraph /\ ( # ` V ) = 1 /\ I : dom I --> E ) /\ U e. V ) -> U e. V )
6 1 2 3 lfuhgr1v0e 
 |-  ( ( G e. UHGraph /\ ( # ` V ) = 1 /\ I : dom I --> E ) -> ( Edg ` G ) = (/) )
7 6 adantr 
 |-  ( ( ( G e. UHGraph /\ ( # ` V ) = 1 /\ I : dom I --> E ) /\ U e. V ) -> ( Edg ` G ) = (/) )
8 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
9 1 8 vtxduhgr0e 
 |-  ( ( G e. UHGraph /\ U e. V /\ ( Edg ` G ) = (/) ) -> ( ( VtxDeg ` G ) ` U ) = 0 )
10 4 5 7 9 syl3anc 
 |-  ( ( ( G e. UHGraph /\ ( # ` V ) = 1 /\ I : dom I --> E ) /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = 0 )
11 10 ex 
 |-  ( ( G e. UHGraph /\ ( # ` V ) = 1 /\ I : dom I --> E ) -> ( U e. V -> ( ( VtxDeg ` G ) ` U ) = 0 ) )