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 = (/) ) )