Description: In a finite simple graph, the number of edges is finite iff the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 9-Nov-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fusgredgfi.v | |
|
fusgredgfi.e | |
||
usgrfilem.f | |
||
Assertion | usgrfilem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fusgredgfi.v | |
|
2 | fusgredgfi.e | |
|
3 | usgrfilem.f | |
|
4 | rabfi | |
|
5 | 3 4 | eqeltrid | |
6 | uncom | |
|
7 | eqid | |
|
8 | 7 3 | elnelun | |
9 | 6 8 | eqtr2i | |
10 | 1 2 | fusgredgfi | |
11 | 10 | anim1ci | |
12 | unfi | |
|
13 | 11 12 | syl | |
14 | 9 13 | eqeltrid | |
15 | 14 | ex | |
16 | 5 15 | impbid2 | |