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 \in USGraph \to (E \in Fin \leftrightarrow I \in 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 \in Fin \leftrightarrow ran I \in Fin$
8	1	fvexi	$⊢ I \in V$
9		eqid	$⊢ Vtx (G) = Vtx (G)$
10	9 1	usgrfs	$⊢ G \in USGraph \to I : dom I \underset{1-1}{⟶} \{x \in 𝒫 Vtx (G) \| \|x\| = 2\}$
11		f1vrnfibi	$⊢ (I \in V \land I : dom I \underset{1-1}{⟶} \{x \in 𝒫 Vtx (G) \| \|x\| = 2\}) \to (I \in Fin \leftrightarrow ran I \in Fin)$
12	8 10 11	sylancr	$⊢ G \in USGraph \to (I \in Fin \leftrightarrow ran I \in Fin)$
13	7 12	bitr4id	$⊢ G \in USGraph \to (E \in Fin \leftrightarrow I \in Fin)$