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