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 ) )