Metamath Proof Explorer

Theorem uhgrvd00

Description: If every vertex in a hypergraph has degree 0, there is no edge in the graph. (Contributed by Alexander van der Vekens, 12-Jul-2018) (Revised by AV, 24-Dec-2020)

Ref Expression
Hypotheses vtxdusgradjvtx.v 
|- V = ( Vtx ` G )
vtxdusgradjvtx.e 
|- E = ( Edg ` G )
Assertion uhgrvd00 
|- ( G e. UHGraph -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = 0 -> E = (/) ) )

Proof

Step Hyp Ref Expression
1 vtxdusgradjvtx.v 
 |-  V = ( Vtx ` G )
2 vtxdusgradjvtx.e 
 |-  E = ( Edg ` G )
3 eqid 
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
4 1 2 3 vtxduhgr0edgnel 
 |-  ( ( G e. UHGraph /\ v e. V ) -> ( ( ( VtxDeg ` G ) ` v ) = 0 <-> -. E. e e. E v e. e ) )
5 ralnex 
 |-  ( A. e e. E -. v e. e <-> -. E. e e. E v e. e )
6 4 5 bitr4di 
 |-  ( ( G e. UHGraph /\ v e. V ) -> ( ( ( VtxDeg ` G ) ` v ) = 0 <-> A. e e. E -. v e. e ) )
7 6 ralbidva 
 |-  ( G e. UHGraph -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = 0 <-> A. v e. V A. e e. E -. v e. e ) )
8 ralcom 
 |-  ( A. v e. V A. e e. E -. v e. e <-> A. e e. E A. v e. V -. v e. e )
9 ralnex2 
 |-  ( A. e e. E A. v e. V -. v e. e <-> -. E. e e. E E. v e. V v e. e )
10 8 9 bitri 
 |-  ( A. v e. V A. e e. E -. v e. e <-> -. E. e e. E E. v e. V v e. e )
11 simpr 
 |-  ( ( G e. UHGraph /\ e e. E ) -> e e. E )
12 2 eleq2i 
 |-  ( e e. E <-> e e. ( Edg ` G ) )
13 uhgredgn0 
 |-  ( ( G e. UHGraph /\ e e. ( Edg ` G ) ) -> e e. ( ~P ( Vtx ` G ) \ { (/) } ) )
14 12 13 sylan2b 
 |-  ( ( G e. UHGraph /\ e e. E ) -> e e. ( ~P ( Vtx ` G ) \ { (/) } ) )
15 eldifsn 
 |-  ( e e. ( ~P ( Vtx ` G ) \ { (/) } ) <-> ( e e. ~P ( Vtx ` G ) /\ e =/= (/) ) )
16 elpwi 
 |-  ( e e. ~P ( Vtx ` G ) -> e C_ ( Vtx ` G ) )
17 1 sseq2i 
 |-  ( e C_ V <-> e C_ ( Vtx ` G ) )
18 ssn0rex 
 |-  ( ( e C_ V /\ e =/= (/) ) -> E. v e. V v e. e )
19 18 ex 
 |-  ( e C_ V -> ( e =/= (/) -> E. v e. V v e. e ) )
20 17 19 sylbir 
 |-  ( e C_ ( Vtx ` G ) -> ( e =/= (/) -> E. v e. V v e. e ) )
21 16 20 syl 
 |-  ( e e. ~P ( Vtx ` G ) -> ( e =/= (/) -> E. v e. V v e. e ) )
22 21 imp 
 |-  ( ( e e. ~P ( Vtx ` G ) /\ e =/= (/) ) -> E. v e. V v e. e )
23 15 22 sylbi 
 |-  ( e e. ( ~P ( Vtx ` G ) \ { (/) } ) -> E. v e. V v e. e )
24 14 23 syl 
 |-  ( ( G e. UHGraph /\ e e. E ) -> E. v e. V v e. e )
25 11 24 jca 
 |-  ( ( G e. UHGraph /\ e e. E ) -> ( e e. E /\ E. v e. V v e. e ) )
26 25 ex 
 |-  ( G e. UHGraph -> ( e e. E -> ( e e. E /\ E. v e. V v e. e ) ) )
27 26 eximdv 
 |-  ( G e. UHGraph -> ( E. e e e. E -> E. e ( e e. E /\ E. v e. V v e. e ) ) )
28 n0 
 |-  ( E =/= (/) <-> E. e e e. E )
29 df-rex 
 |-  ( E. e e. E E. v e. V v e. e <-> E. e ( e e. E /\ E. v e. V v e. e ) )
30 27 28 29 3imtr4g 
 |-  ( G e. UHGraph -> ( E =/= (/) -> E. e e. E E. v e. V v e. e ) )
31 30 con3d 
 |-  ( G e. UHGraph -> ( -. E. e e. E E. v e. V v e. e -> -. E =/= (/) ) )
32 10 31 syl5bi 
 |-  ( G e. UHGraph -> ( A. v e. V A. e e. E -. v e. e -> -. E =/= (/) ) )
33 nne 
 |-  ( -. E =/= (/) <-> E = (/) )
34 32 33 syl6ib 
 |-  ( G e. UHGraph -> ( A. v e. V A. e e. E -. v e. e -> E = (/) ) )
35 7 34 sylbid 
 |-  ( G e. UHGraph -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = 0 -> E = (/) ) )