Metamath Proof Explorer

Theorem vtxd0nedgb

Description: A vertex has degree 0 iff there is no edge incident with the vertex. (Contributed by AV, 24-Dec-2020) (Revised by AV, 22-Mar-2021)

Ref Expression
Hypotheses vtxd0nedgb.v 
|- V = ( Vtx ` G )
vtxd0nedgb.i 
|- I = ( iEdg ` G )
vtxd0nedgb.d 
|- D = ( VtxDeg ` G )
Assertion vtxd0nedgb 
|- ( U e. V -> ( ( D ` U ) = 0 <-> -. E. i e. dom I U e. ( I ` i ) ) )

Proof

Step Hyp Ref Expression
1 vtxd0nedgb.v 
 |-  V = ( Vtx ` G )
2 vtxd0nedgb.i 
 |-  I = ( iEdg ` G )
3 vtxd0nedgb.d 
 |-  D = ( VtxDeg ` G )
4 3 fveq1i 
 |-  ( D ` U ) = ( ( VtxDeg ` G ) ` U )
5 eqid 
 |-  dom I = dom I
6 1 2 5 vtxdgval 
 |-  ( U e. V -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { i e. dom I | U e. ( I ` i ) } ) +e ( # ` { i e. dom I | ( I ` i ) = { U } } ) ) )
7 4 6 eqtrid 
 |-  ( U e. V -> ( D ` U ) = ( ( # ` { i e. dom I | U e. ( I ` i ) } ) +e ( # ` { i e. dom I | ( I ` i ) = { U } } ) ) )
8 7 eqeq1d 
 |-  ( U e. V -> ( ( D ` U ) = 0 <-> ( ( # ` { i e. dom I | U e. ( I ` i ) } ) +e ( # ` { i e. dom I | ( I ` i ) = { U } } ) ) = 0 ) )
9 2 fvexi 
 |-  I e. _V
10 9 dmex 
 |-  dom I e. _V
11 10 rabex 
 |-  { i e. dom I | U e. ( I ` i ) } e. _V
12 hashxnn0 
 |-  ( { i e. dom I | U e. ( I ` i ) } e. _V -> ( # ` { i e. dom I | U e. ( I ` i ) } ) e. NN0* )
13 11 12 ax-mp 
 |-  ( # ` { i e. dom I | U e. ( I ` i ) } ) e. NN0*
14 10 rabex 
 |-  { i e. dom I | ( I ` i ) = { U } } e. _V
15 hashxnn0 
 |-  ( { i e. dom I | ( I ` i ) = { U } } e. _V -> ( # ` { i e. dom I | ( I ` i ) = { U } } ) e. NN0* )
16 14 15 ax-mp 
 |-  ( # ` { i e. dom I | ( I ` i ) = { U } } ) e. NN0*
17 13 16 pm3.2i 
 |-  ( ( # ` { i e. dom I | U e. ( I ` i ) } ) e. NN0* /\ ( # ` { i e. dom I | ( I ` i ) = { U } } ) e. NN0* )
18 xnn0xadd0 
 |-  ( ( ( # ` { i e. dom I | U e. ( I ` i ) } ) e. NN0* /\ ( # ` { i e. dom I | ( I ` i ) = { U } } ) e. NN0* ) -> ( ( ( # ` { i e. dom I | U e. ( I ` i ) } ) +e ( # ` { i e. dom I | ( I ` i ) = { U } } ) ) = 0 <-> ( ( # ` { i e. dom I | U e. ( I ` i ) } ) = 0 /\ ( # ` { i e. dom I | ( I ` i ) = { U } } ) = 0 ) ) )
19 17 18 mp1i 
 |-  ( U e. V -> ( ( ( # ` { i e. dom I | U e. ( I ` i ) } ) +e ( # ` { i e. dom I | ( I ` i ) = { U } } ) ) = 0 <-> ( ( # ` { i e. dom I | U e. ( I ` i ) } ) = 0 /\ ( # ` { i e. dom I | ( I ` i ) = { U } } ) = 0 ) ) )
20 hasheq0 
 |-  ( { i e. dom I | U e. ( I ` i ) } e. _V -> ( ( # ` { i e. dom I | U e. ( I ` i ) } ) = 0 <-> { i e. dom I | U e. ( I ` i ) } = (/) ) )
21 11 20 ax-mp 
 |-  ( ( # ` { i e. dom I | U e. ( I ` i ) } ) = 0 <-> { i e. dom I | U e. ( I ` i ) } = (/) )
22 hasheq0 
 |-  ( { i e. dom I | ( I ` i ) = { U } } e. _V -> ( ( # ` { i e. dom I | ( I ` i ) = { U } } ) = 0 <-> { i e. dom I | ( I ` i ) = { U } } = (/) ) )
23 14 22 ax-mp 
 |-  ( ( # ` { i e. dom I | ( I ` i ) = { U } } ) = 0 <-> { i e. dom I | ( I ` i ) = { U } } = (/) )
24 21 23 anbi12i 
 |-  ( ( ( # ` { i e. dom I | U e. ( I ` i ) } ) = 0 /\ ( # ` { i e. dom I | ( I ` i ) = { U } } ) = 0 ) <-> ( { i e. dom I | U e. ( I ` i ) } = (/) /\ { i e. dom I | ( I ` i ) = { U } } = (/) ) )
25 rabeq0 
 |-  ( { i e. dom I | U e. ( I ` i ) } = (/) <-> A. i e. dom I -. U e. ( I ` i ) )
26 rabeq0 
 |-  ( { i e. dom I | ( I ` i ) = { U } } = (/) <-> A. i e. dom I -. ( I ` i ) = { U } )
27 25 26 anbi12i 
 |-  ( ( { i e. dom I | U e. ( I ` i ) } = (/) /\ { i e. dom I | ( I ` i ) = { U } } = (/) ) <-> ( A. i e. dom I -. U e. ( I ` i ) /\ A. i e. dom I -. ( I ` i ) = { U } ) )
28 ralnex 
 |-  ( A. i e. dom I -. ( U e. ( I ` i ) \/ ( I ` i ) = { U } ) <-> -. E. i e. dom I ( U e. ( I ` i ) \/ ( I ` i ) = { U } ) )
29 28 bicomi 
 |-  ( -. E. i e. dom I ( U e. ( I ` i ) \/ ( I ` i ) = { U } ) <-> A. i e. dom I -. ( U e. ( I ` i ) \/ ( I ` i ) = { U } ) )
30 ioran 
 |-  ( -. ( U e. ( I ` i ) \/ ( I ` i ) = { U } ) <-> ( -. U e. ( I ` i ) /\ -. ( I ` i ) = { U } ) )
31 30 ralbii 
 |-  ( A. i e. dom I -. ( U e. ( I ` i ) \/ ( I ` i ) = { U } ) <-> A. i e. dom I ( -. U e. ( I ` i ) /\ -. ( I ` i ) = { U } ) )
32 r19.26 
 |-  ( A. i e. dom I ( -. U e. ( I ` i ) /\ -. ( I ` i ) = { U } ) <-> ( A. i e. dom I -. U e. ( I ` i ) /\ A. i e. dom I -. ( I ` i ) = { U } ) )
33 29 31 32 3bitri 
 |-  ( -. E. i e. dom I ( U e. ( I ` i ) \/ ( I ` i ) = { U } ) <-> ( A. i e. dom I -. U e. ( I ` i ) /\ A. i e. dom I -. ( I ` i ) = { U } ) )
34 33 bicomi 
 |-  ( ( A. i e. dom I -. U e. ( I ` i ) /\ A. i e. dom I -. ( I ` i ) = { U } ) <-> -. E. i e. dom I ( U e. ( I ` i ) \/ ( I ` i ) = { U } ) )
35 24 27 34 3bitri 
 |-  ( ( ( # ` { i e. dom I | U e. ( I ` i ) } ) = 0 /\ ( # ` { i e. dom I | ( I ` i ) = { U } } ) = 0 ) <-> -. E. i e. dom I ( U e. ( I ` i ) \/ ( I ` i ) = { U } ) )
36 orcom 
 |-  ( ( U e. ( I ` i ) \/ ( I ` i ) = { U } ) <-> ( ( I ` i ) = { U } \/ U e. ( I ` i ) ) )
37 snidg 
 |-  ( U e. V -> U e. { U } )
38 eleq2 
 |-  ( ( I ` i ) = { U } -> ( U e. ( I ` i ) <-> U e. { U } ) )
39 37 38 syl5ibrcom 
 |-  ( U e. V -> ( ( I ` i ) = { U } -> U e. ( I ` i ) ) )
40 pm4.72 
 |-  ( ( ( I ` i ) = { U } -> U e. ( I ` i ) ) <-> ( U e. ( I ` i ) <-> ( ( I ` i ) = { U } \/ U e. ( I ` i ) ) ) )
41 39 40 sylib 
 |-  ( U e. V -> ( U e. ( I ` i ) <-> ( ( I ` i ) = { U } \/ U e. ( I ` i ) ) ) )
42 36 41 bitr4id 
 |-  ( U e. V -> ( ( U e. ( I ` i ) \/ ( I ` i ) = { U } ) <-> U e. ( I ` i ) ) )
43 42 rexbidv 
 |-  ( U e. V -> ( E. i e. dom I ( U e. ( I ` i ) \/ ( I ` i ) = { U } ) <-> E. i e. dom I U e. ( I ` i ) ) )
44 43 notbid 
 |-  ( U e. V -> ( -. E. i e. dom I ( U e. ( I ` i ) \/ ( I ` i ) = { U } ) <-> -. E. i e. dom I U e. ( I ` i ) ) )
45 35 44 syl5bb 
 |-  ( U e. V -> ( ( ( # ` { i e. dom I | U e. ( I ` i ) } ) = 0 /\ ( # ` { i e. dom I | ( I ` i ) = { U } } ) = 0 ) <-> -. E. i e. dom I U e. ( I ` i ) ) )
46 8 19 45 3bitrd 
 |-  ( U e. V -> ( ( D ` U ) = 0 <-> -. E. i e. dom I U e. ( I ` i ) ) )