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-1 x 𝒫 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-1 x 𝒫 V | x = 2
5 4 anbi1d G W G USGraph V Fin I : dom I 1-1 x 𝒫 V | x = 2 V Fin
6 3 5 syl5bb G W G FinUSGraph I : dom I 1-1 x 𝒫 V | x = 2 V Fin