Metamath Proof Explorer

Theorem isfusgrf1

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

Ref Expression
Hypotheses isfusgr.v ⊢V=Vtx⁡G
isfusgrf1.i ⊢I=iEdg⁡G
Assertion isfusgrf1 ⊢G∈W→G∈FinUSGraph↔I:dom⁡I⟶1-1x∈𝒫V|x=2∧V∈Fin

Proof

Step Hyp Ref Expression
1 isfusgr.v ⊢V=Vtx⁡G
2 isfusgrf1.i ⊢I=iEdg⁡G
3 1 isfusgr ⊢G∈FinUSGraph↔G∈USGraph∧V∈Fin
4 1 2 isusgrs ⊢G∈W→G∈USGraph↔I:dom⁡I⟶1-1x∈𝒫V|x=2
5 4 anbi1d ⊢G∈W→G∈USGraph∧V∈Fin↔I:dom⁡I⟶1-1x∈𝒫V|x=2∧V∈Fin
6 3 5 bitrid ⊢G∈W→G∈FinUSGraph↔I:dom⁡I⟶1-1x∈𝒫V|x=2∧V∈Fin