This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 bitrid 
 |-  ( ( 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 ) )