Metamath Proof Explorer

Theorem isfusgrcl

Description: The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020) (Revised by AV, 9-Jan-2020)

Ref Expression
Assertion isfusgrcl 
|- ( G e. FinUSGraph <-> ( G e. USGraph /\ ( # ` ( Vtx ` G ) ) e. NN0 ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 isfusgr 
 |-  ( G e. FinUSGraph <-> ( G e. USGraph /\ ( Vtx ` G ) e. Fin ) )
3 fvex 
 |-  ( Vtx ` G ) e. _V
4 hashclb 
 |-  ( ( Vtx ` G ) e. _V -> ( ( Vtx ` G ) e. Fin <-> ( # ` ( Vtx ` G ) ) e. NN0 ) )
5 3 4 mp1i 
 |-  ( G e. USGraph -> ( ( Vtx ` G ) e. Fin <-> ( # ` ( Vtx ` G ) ) e. NN0 ) )
6 5 pm5.32i 
 |-  ( ( G e. USGraph /\ ( Vtx ` G ) e. Fin ) <-> ( G e. USGraph /\ ( # ` ( Vtx ` G ) ) e. NN0 ) )
7 2 6 bitri 
 |-  ( G e. FinUSGraph <-> ( G e. USGraph /\ ( # ` ( Vtx ` G ) ) e. NN0 ) )