Metamath Proof Explorer

Theorem uhgredgrnv

Description: An edge of a hypergraph contains only vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 4-Jun-2021)

Ref Expression
Assertion uhgredgrnv 
|- ( ( G e. UHGraph /\ E e. ( Edg ` G ) /\ N e. E ) -> N e. ( Vtx ` G ) )

Proof

Step Hyp Ref Expression
1 edguhgr 
 |-  ( ( G e. UHGraph /\ E e. ( Edg ` G ) ) -> E e. ~P ( Vtx ` G ) )
2 elelpwi 
 |-  ( ( N e. E /\ E e. ~P ( Vtx ` G ) ) -> N e. ( Vtx ` G ) )
3 2 expcom 
 |-  ( E e. ~P ( Vtx ` G ) -> ( N e. E -> N e. ( Vtx ` G ) ) )
4 1 3 syl 
 |-  ( ( G e. UHGraph /\ E e. ( Edg ` G ) ) -> ( N e. E -> N e. ( Vtx ` G ) ) )
5 4 3impia 
 |-  ( ( G e. UHGraph /\ E e. ( Edg ` G ) /\ N e. E ) -> N e. ( Vtx ` G ) )