Metamath Proof Explorer

Theorem fusgrfupgrfs

Description: A finite simple graph is a finite pseudograph of finite size. (Contributed by AV, 27-Dec-2021)

Ref Expression
Hypotheses fusgrfupgrfs.v ⊢V=Vtx⁡G
fusgrfupgrfs.i ⊢I=iEdg⁡G
Assertion fusgrfupgrfs ⊢G∈FinUSGraph→G∈UPGraph∧V∈Fin∧I∈Fin

Proof

Step Hyp Ref Expression
1 fusgrfupgrfs.v ⊢V=Vtx⁡G
2 fusgrfupgrfs.i ⊢I=iEdg⁡G
3 fusgrusgr ⊢G∈FinUSGraph→G∈USGraph
4 usgrupgr ⊢G∈USGraph→G∈UPGraph
5 3 4 syl ⊢G∈FinUSGraph→G∈UPGraph
6 1 fusgrvtxfi ⊢G∈FinUSGraph→V∈Fin
7 fusgrfis ⊢G∈FinUSGraph→Edg⁡G∈Fin
8 eqid ⊢Edg⁡G=Edg⁡G
9 2 8 usgredgffibi ⊢G∈USGraph→Edg⁡G∈Fin↔I∈Fin
10 3 9 syl ⊢G∈FinUSGraph→Edg⁡G∈Fin↔I∈Fin
11 7 10 mpbid ⊢G∈FinUSGraph→I∈Fin
12 5 6 11 3jca ⊢G∈FinUSGraph→G∈UPGraph∧V∈Fin∧I∈Fin