Theorem vtxdusgr0edgnelALT

Description: Alternate proof of vtxdusgr0edgnel , not based on vtxduhgr0edgnel . A vertex in a simple graph has degree 0 if there is no edge incident with this vertex. (Contributed by AV, 17-Dec-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	vtxdushgrfvedg.v	|- V = ( Vtx ` G )
	vtxdushgrfvedg.e	|- E = ( Edg ` G )
	vtxdushgrfvedg.d	|- D = ( VtxDeg ` G )
Assertion	vtxdusgr0edgnelALT	|- ( ( G e. USGraph /\ U e. V ) -> ( ( D ` U ) = 0 <-> -. E. e e. E U 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	1 2 3	vtxdusgrfvedg	|- ( ( G e. USGraph /\ U e. V ) -> ( D ` U ) = ( # ` { e e. E | U e. e } ) )
5	4	eqeq1d	|- ( ( G e. USGraph /\ U e. V ) -> ( ( D ` U ) = 0 <-> ( # ` { e e. E | U e. e } ) = 0 ) )
6		fvex	|- ( Edg ` G ) e. _V
7	2 6	eqeltri	|- E e. _V
8	7	rabex	|- { e e. E | U e. e } e. _V
9		hasheq0	|- ( { e e. E | U e. e } e. _V -> ( ( # ` { e e. E | U e. e } ) = 0 <-> { e e. E | U e. e } = (/) ) )
10	8 9	mp1i	|- ( ( G e. USGraph /\ U e. V ) -> ( ( # ` { e e. E | U e. e } ) = 0 <-> { e e. E | U e. e } = (/) ) )
11		rabeq0	|- ( { e e. E | U e. e } = (/) <-> A. e e. E -. U e. e )
12		ralnex	|- ( A. e e. E -. U e. e <-> -. E. e e. E U e. e )
13	12	a1i	|- ( ( G e. USGraph /\ U e. V ) -> ( A. e e. E -. U e. e <-> -. E. e e. E U e. e ) )
14	11 13	syl5bb	|- ( ( G e. USGraph /\ U e. V ) -> ( { e e. E | U e. e } = (/) <-> -. E. e e. E U e. e ) )
15	5 10 14	3bitrd	|- ( ( G e. USGraph /\ U e. V ) -> ( ( D ` U ) = 0 <-> -. E. e e. E U e. e ) )