Theorem usgrvd0nedg

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

	Ref	Expression
Hypotheses	vtxdusgradjvtx.v	|- V = ( Vtx ` G )
	vtxdusgradjvtx.e	|- E = ( Edg ` G )
Assertion	usgrvd0nedg	|- ( ( G e. USGraph /\ U e. V ) -> ( ( ( VtxDeg ` G ) ` U ) = 0 -> -. E. v e. V { U , v } e. E ) )

Proof

Step	Hyp	Ref	Expression
1		vtxdusgradjvtx.v	|- V = ( Vtx ` G )
2		vtxdusgradjvtx.e	|- E = ( Edg ` G )
3	1 2	vtxdusgradjvtx	|- ( ( G e. USGraph /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = ( # ` { v e. V | { U , v } e. E } ) )
4	3	eqeq1d	|- ( ( G e. USGraph /\ U e. V ) -> ( ( ( VtxDeg ` G ) ` U ) = 0 <-> ( # ` { v e. V | { U , v } e. E } ) = 0 ) )
5	1	fvexi	|- V e. _V
6	5	rabex	|- { v e. V | { U , v } e. E } e. _V
7		hasheq0	|- ( { v e. V | { U , v } e. E } e. _V -> ( ( # ` { v e. V | { U , v } e. E } ) = 0 <-> { v e. V | { U , v } e. E } = (/) ) )
8	6 7	ax-mp	|- ( ( # ` { v e. V | { U , v } e. E } ) = 0 <-> { v e. V | { U , v } e. E } = (/) )
9		rabeq0	|- ( { v e. V | { U , v } e. E } = (/) <-> A. v e. V -. { U , v } e. E )
10		ralnex	|- ( A. v e. V -. { U , v } e. E <-> -. E. v e. V { U , v } e. E )
11	10	biimpi	|- ( A. v e. V -. { U , v } e. E -> -. E. v e. V { U , v } e. E )
12	11	a1i	|- ( ( G e. USGraph /\ U e. V ) -> ( A. v e. V -. { U , v } e. E -> -. E. v e. V { U , v } e. E ) )
13	9 12	biimtrid	|- ( ( G e. USGraph /\ U e. V ) -> ( { v e. V | { U , v } e. E } = (/) -> -. E. v e. V { U , v } e. E ) )
14	8 13	biimtrid	|- ( ( G e. USGraph /\ U e. V ) -> ( ( # ` { v e. V | { U , v } e. E } ) = 0 -> -. E. v e. V { U , v } e. E ) )
15	4 14	sylbid	|- ( ( G e. USGraph /\ U e. V ) -> ( ( ( VtxDeg ` G ) ` U ) = 0 -> -. E. v e. V { U , v } e. E ) )