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