Metamath Proof Explorer


Theorem usgredgffibi

Description: The number of edges in a simple graph is finite iff its edge function is finite. (Contributed by AV, 10-Jan-2020) (Revised by AV, 22-Oct-2020)

Ref Expression
Hypotheses usgredgffibi.I 𝐼 = ( iEdg ‘ 𝐺 )
usgredgffibi.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion usgredgffibi ( 𝐺 ∈ USGraph → ( 𝐸 ∈ Fin ↔ 𝐼 ∈ Fin ) )

Proof

Step Hyp Ref Expression
1 usgredgffibi.I 𝐼 = ( iEdg ‘ 𝐺 )
2 usgredgffibi.e 𝐸 = ( Edg ‘ 𝐺 )
3 edgval ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
4 1 eqcomi ( iEdg ‘ 𝐺 ) = 𝐼
5 4 rneqi ran ( iEdg ‘ 𝐺 ) = ran 𝐼
6 2 3 5 3eqtri 𝐸 = ran 𝐼
7 6 eleq1i ( 𝐸 ∈ Fin ↔ ran 𝐼 ∈ Fin )
8 1 fvexi 𝐼 ∈ V
9 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
10 9 1 usgrfs ( 𝐺 ∈ USGraph → 𝐼 : dom 𝐼1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
11 f1vrnfibi ( ( 𝐼 ∈ V ∧ 𝐼 : dom 𝐼1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) → ( 𝐼 ∈ Fin ↔ ran 𝐼 ∈ Fin ) )
12 8 10 11 sylancr ( 𝐺 ∈ USGraph → ( 𝐼 ∈ Fin ↔ ran 𝐼 ∈ Fin ) )
13 7 12 bitr4id ( 𝐺 ∈ USGraph → ( 𝐸 ∈ Fin ↔ 𝐼 ∈ Fin ) )