This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐼 = ( 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 𝐼 → ( 𝐸 = ∅ ↔ 𝐼 = ∅ ) )