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 ⊢ I = iEdg ⁡ G
usgredgffibi.e ⊢ E = Edg ⁡ G
Assertion usgredgffibi ⊢ G ∈ USGraph → E ∈ Fin ↔ I ∈ Fin

Proof

Step Hyp Ref Expression
1 usgredgffibi.I ⊢ I = iEdg ⁡ G
2 usgredgffibi.e ⊢ E = Edg ⁡ G
3 1 fvexi ⊢ I ∈ V
4 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
5 4 1 usgrfs ⊢ G ∈ USGraph → I : dom ⁡ I ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G | x = 2
6 f1vrnfibi ⊢ I ∈ V ∧ I : dom ⁡ I ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G | x = 2 → I ∈ Fin ↔ ran ⁡ I ∈ Fin
7 3 5 6 sylancr ⊢ G ∈ USGraph → I ∈ Fin ↔ ran ⁡ I ∈ Fin
8 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
9 1 eqcomi ⊢ iEdg ⁡ G = I
10 9 rneqi ⊢ ran ⁡ iEdg ⁡ G = ran ⁡ I
11 2 8 10 3eqtri ⊢ E = ran ⁡ I
12 11 eleq1i ⊢ E ∈ Fin ↔ ran ⁡ I ∈ Fin
13 7 12 syl6rbbr ⊢ G ∈ USGraph → E ∈ Fin ↔ I ∈ Fin