Metamath Proof Explorer

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 = iEdg ⁡ G
edg0iedg0.e ⊢ E = Edg ⁡ G
Assertion edg0iedg0 ⊢ Fun ⁡ I → E = ∅ ↔ I = ∅

Proof

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