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	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	edg0iedg0.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	edg0iedg0	⊢ ( Fun 𝐼 → ( 𝐸 = ∅ ↔ 𝐼 = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		edg0iedg0.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2		edg0iedg0.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		edgval	⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
4	2 3	eqtri	⊢ 𝐸 = ran ( iEdg ‘ 𝐺 )
5	4	eqeq1i	⊢ ( 𝐸 = ∅ ↔ ran ( iEdg ‘ 𝐺 ) = ∅ )
6	5	a1i	⊢ ( Fun 𝐼 → ( 𝐸 = ∅ ↔ ran ( iEdg ‘ 𝐺 ) = ∅ ) )
7	1	eqcomi	⊢ ( iEdg ‘ 𝐺 ) = 𝐼
8	7	rneqi	⊢ ran ( iEdg ‘ 𝐺 ) = ran 𝐼
9	8	eqeq1i	⊢ ( ran ( iEdg ‘ 𝐺 ) = ∅ ↔ ran 𝐼 = ∅ )
10	9	a1i	⊢ ( Fun 𝐼 → ( ran ( iEdg ‘ 𝐺 ) = ∅ ↔ ran 𝐼 = ∅ ) )
11		funrel	⊢ ( Fun 𝐼 → Rel 𝐼 )
12		relrn0	⊢ ( Rel 𝐼 → ( 𝐼 = ∅ ↔ ran 𝐼 = ∅ ) )
13	12	bicomd	⊢ ( Rel 𝐼 → ( ran 𝐼 = ∅ ↔ 𝐼 = ∅ ) )
14	11 13	syl	⊢ ( Fun 𝐼 → ( ran 𝐼 = ∅ ↔ 𝐼 = ∅ ) )
15	6 10 14	3bitrd	⊢ ( Fun 𝐼 → ( 𝐸 = ∅ ↔ 𝐼 = ∅ ) )