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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
fusgrfupgrfs.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion fusgrfupgrfs ( 𝐺 ∈ FinUSGraph → ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) )

Proof

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