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