Theorem edg0iedg0

Description: There is no edge in a graph iff its edge function is empty. (Contributed by AV, 15-Dec-2020) (Revised by AV, 8-Dec-2021)

	Ref	Expression
Hypotheses	edg0iedg0.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	edg0iedg0.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	edg0iedg0	$$⊢\mathrm{Fun}I\to \left(E=\varnothing \leftrightarrow I=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		edg0iedg0.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
2		edg0iedg0.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
3		edgval	$$⊢\mathrm{Edg}\left(G\right)=\mathrm{ran}\mathrm{iEdg}\left(G\right)$$
4	2 3	eqtri	$$⊢E=\mathrm{ran}\mathrm{iEdg}\left(G\right)$$
5	4	eqeq1i	$$⊢E=\varnothing \leftrightarrow \mathrm{ran}\mathrm{iEdg}\left(G\right)=\varnothing$$
6	5	a1i	$$⊢\mathrm{Fun}I\to \left(E=\varnothing \leftrightarrow \mathrm{ran}\mathrm{iEdg}\left(G\right)=\varnothing \right)$$
7	1	eqcomi	$$⊢\mathrm{iEdg}\left(G\right)=I$$
8	7	rneqi	$$⊢\mathrm{ran}\mathrm{iEdg}\left(G\right)=\mathrm{ran}I$$
9	8	eqeq1i	$$⊢\mathrm{ran}\mathrm{iEdg}\left(G\right)=\varnothing \leftrightarrow \mathrm{ran}I=\varnothing$$
10	9	a1i	$$⊢\mathrm{Fun}I\to \left(\mathrm{ran}\mathrm{iEdg}\left(G\right)=\varnothing \leftrightarrow \mathrm{ran}I=\varnothing \right)$$
11		funrel	$$⊢\mathrm{Fun}I\to \mathrm{Rel}I$$
12		relrn0	$$⊢\mathrm{Rel}I\to \left(I=\varnothing \leftrightarrow \mathrm{ran}I=\varnothing \right)$$
13	12	bicomd	$$⊢\mathrm{Rel}I\to \left(\mathrm{ran}I=\varnothing \leftrightarrow I=\varnothing \right)$$
14	11 13	syl	$$⊢\mathrm{Fun}I\to \left(\mathrm{ran}I=\varnothing \leftrightarrow I=\varnothing \right)$$
15	6 10 14	3bitrd	$$⊢\mathrm{Fun}I\to \left(E=\varnothing \leftrightarrow I=\varnothing \right)$$