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∈FinUSGraph↔G∈USGraph∧Vtx⁡G∈ℕ0

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 1 isfusgr ⊢G∈FinUSGraph↔G∈USGraph∧Vtx⁡G∈Fin
3 fvex ⊢Vtx⁡G∈V
4 hashclb ⊢Vtx⁡G∈V→Vtx⁡G∈Fin↔Vtx⁡G∈ℕ0
5 3 4 mp1i ⊢G∈USGraph→Vtx⁡G∈Fin↔Vtx⁡G∈ℕ0
6 5 pm5.32i ⊢G∈USGraph∧Vtx⁡G∈Fin↔G∈USGraph∧Vtx⁡G∈ℕ0
7 2 6 bitri ⊢G∈FinUSGraph↔G∈USGraph∧Vtx⁡G∈ℕ0