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 ∈ FinUSGraph ↔ G ∈ USGraph ∧ V ∈ 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 ∈ Fin ↔ V ∈ Fin
5 df-fusgr ⊢ FinUSGraph = g ∈ USGraph | Vtx ⁡ g ∈ Fin
6 4 5 elrab2 ⊢ G ∈ FinUSGraph ↔ G ∈ USGraph ∧ V ∈ Fin