This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. FinUSGraph -> ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) )

Proof

Step Hyp Ref Expression
1 fusgrfupgrfs.v 
 |-  V = ( Vtx ` G )
2 fusgrfupgrfs.i 
 |-  I = ( iEdg ` G )
3 fusgrusgr 
 |-  ( G e. FinUSGraph -> G e. USGraph )
4 usgrupgr 
 |-  ( G e. USGraph -> G e. UPGraph )
5 3 4 syl 
 |-  ( G e. FinUSGraph -> G e. UPGraph )
6 1 fusgrvtxfi 
 |-  ( G e. FinUSGraph -> V e. Fin )
7 fusgrfis 
 |-  ( G e. FinUSGraph -> ( Edg ` G ) e. Fin )
8 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
9 2 8 usgredgffibi 
 |-  ( G e. USGraph -> ( ( Edg ` G ) e. Fin <-> I e. Fin ) )
10 3 9 syl 
 |-  ( G e. FinUSGraph -> ( ( Edg ` G ) e. Fin <-> I e. Fin ) )
11 7 10 mpbid 
 |-  ( G e. FinUSGraph -> I e. Fin )
12 5 6 11 3jca 
 |-  ( G e. FinUSGraph -> ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) )