Description: The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020) (Revised by AV, 21-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | isfusgr.v | |- V = ( Vtx ` G ) |
|
Assertion | isfusgr | |- ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isfusgr.v | |- V = ( Vtx ` G ) |
|
2 | fveq2 | |- ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) ) |
|
3 | 2 1 | eqtr4di | |- ( g = G -> ( Vtx ` g ) = V ) |
4 | 3 | eleq1d | |- ( g = G -> ( ( Vtx ` g ) e. Fin <-> V e. Fin ) ) |
5 | df-fusgr | |- FinUSGraph = { g e. USGraph | ( Vtx ` g ) e. Fin } |
|
6 | 4 5 | elrab2 | |- ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) ) |