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 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
4 1 eqcomi ⊢ iEdg ⁡ G = I
5 4 rneqi ⊢ ran ⁡ iEdg ⁡ G = ran ⁡ I
6 2 3 5 3eqtri ⊢ E = ran ⁡ I
7 6 eleq1i ⊢ E ∈ Fin ↔ ran ⁡ I ∈ Fin
8 1 fvexi ⊢ I ∈ V
9 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
10 9 1 usgrfs ⊢ G ∈ USGraph → I : dom ⁡ I ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G | x = 2
11 f1vrnfibi ⊢ I ∈ V ∧ I : dom ⁡ I ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G | x = 2 → I ∈ Fin ↔ ran ⁡ I ∈ Fin
12 8 10 11 sylancr ⊢ G ∈ USGraph → I ∈ Fin ↔ ran ⁡ I ∈ Fin
13 7 12 bitr4id ⊢ G ∈ USGraph → E ∈ Fin ↔ I ∈ Fin