Metamath Proof Explorer


Theorem isfusgr

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

Proof

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