Metamath Proof Explorer

Theorem vtxduhgr0nedg

Description: If a vertex in a hypergraph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017) (Revised by AV, 15-Dec-2020) (Proof shortened by AV, 24-Dec-2020)

Ref Expression
Hypotheses vtxdushgrfvedg.v 
|- V = ( Vtx ` G )
vtxdushgrfvedg.e 
|- E = ( Edg ` G )
vtxdushgrfvedg.d 
|- D = ( VtxDeg ` G )
Assertion vtxduhgr0nedg 
|- ( ( G e. UHGraph /\ U e. V /\ ( D ` U ) = 0 ) -> -. E. v e. V { U , v } e. E )

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v 
 |-  V = ( Vtx ` G )
2 vtxdushgrfvedg.e 
 |-  E = ( Edg ` G )
3 vtxdushgrfvedg.d 
 |-  D = ( VtxDeg ` G )
4 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
5 1 4 3 vtxd0nedgb 
 |-  ( U e. V -> ( ( D ` U ) = 0 <-> -. E. i e. dom ( iEdg ` G ) U e. ( ( iEdg ` G ) ` i ) ) )
6 5 adantl 
 |-  ( ( G e. UHGraph /\ U e. V ) -> ( ( D ` U ) = 0 <-> -. E. i e. dom ( iEdg ` G ) U e. ( ( iEdg ` G ) ` i ) ) )
7 2 eleq2i 
 |-  ( { U , v } e. E <-> { U , v } e. ( Edg ` G ) )
8 4 uhgredgiedgb 
 |-  ( G e. UHGraph -> ( { U , v } e. ( Edg ` G ) <-> E. i e. dom ( iEdg ` G ) { U , v } = ( ( iEdg ` G ) ` i ) ) )
9 7 8 syl5bb 
 |-  ( G e. UHGraph -> ( { U , v } e. E <-> E. i e. dom ( iEdg ` G ) { U , v } = ( ( iEdg ` G ) ` i ) ) )
10 9 adantr 
 |-  ( ( G e. UHGraph /\ U e. V ) -> ( { U , v } e. E <-> E. i e. dom ( iEdg ` G ) { U , v } = ( ( iEdg ` G ) ` i ) ) )
11 prid1g 
 |-  ( U e. V -> U e. { U , v } )
12 eleq2 
 |-  ( { U , v } = ( ( iEdg ` G ) ` i ) -> ( U e. { U , v } <-> U e. ( ( iEdg ` G ) ` i ) ) )
13 11 12 syl5ibcom 
 |-  ( U e. V -> ( { U , v } = ( ( iEdg ` G ) ` i ) -> U e. ( ( iEdg ` G ) ` i ) ) )
14 13 adantl 
 |-  ( ( G e. UHGraph /\ U e. V ) -> ( { U , v } = ( ( iEdg ` G ) ` i ) -> U e. ( ( iEdg ` G ) ` i ) ) )
15 14 reximdv 
 |-  ( ( G e. UHGraph /\ U e. V ) -> ( E. i e. dom ( iEdg ` G ) { U , v } = ( ( iEdg ` G ) ` i ) -> E. i e. dom ( iEdg ` G ) U e. ( ( iEdg ` G ) ` i ) ) )
16 10 15 sylbid 
 |-  ( ( G e. UHGraph /\ U e. V ) -> ( { U , v } e. E -> E. i e. dom ( iEdg ` G ) U e. ( ( iEdg ` G ) ` i ) ) )
17 16 rexlimdvw 
 |-  ( ( G e. UHGraph /\ U e. V ) -> ( E. v e. V { U , v } e. E -> E. i e. dom ( iEdg ` G ) U e. ( ( iEdg ` G ) ` i ) ) )
18 17 con3d 
 |-  ( ( G e. UHGraph /\ U e. V ) -> ( -. E. i e. dom ( iEdg ` G ) U e. ( ( iEdg ` G ) ` i ) -> -. E. v e. V { U , v } e. E ) )
19 6 18 sylbid 
 |-  ( ( G e. UHGraph /\ U e. V ) -> ( ( D ` U ) = 0 -> -. E. v e. V { U , v } e. E ) )
20 19 3impia 
 |-  ( ( G e. UHGraph /\ U e. V /\ ( D ` U ) = 0 ) -> -. E. v e. V { U , v } e. E )