Metamath Proof Explorer


Theorem edg0usgr

Description: A class without edges is a simple graph. Since ran F = (/) does not generally imply Fun F , but Fun ( iEdgG ) is required for G to be a simple graph, however, this must be provided as assertion. (Contributed by AV, 18-Oct-2020)

Ref Expression
Assertion edg0usgr ( ( 𝐺𝑊 ∧ ( Edg ‘ 𝐺 ) = ∅ ∧ Fun ( iEdg ‘ 𝐺 ) ) → 𝐺 ∈ USGraph )

Proof

Step Hyp Ref Expression
1 edgval ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
2 1 a1i ( 𝐺𝑊 → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
3 2 eqeq1d ( 𝐺𝑊 → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ran ( iEdg ‘ 𝐺 ) = ∅ ) )
4 funrel ( Fun ( iEdg ‘ 𝐺 ) → Rel ( iEdg ‘ 𝐺 ) )
5 relrn0 ( Rel ( iEdg ‘ 𝐺 ) → ( ( iEdg ‘ 𝐺 ) = ∅ ↔ ran ( iEdg ‘ 𝐺 ) = ∅ ) )
6 5 bicomd ( Rel ( iEdg ‘ 𝐺 ) → ( ran ( iEdg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
7 4 6 syl ( Fun ( iEdg ‘ 𝐺 ) → ( ran ( iEdg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
8 simpr ( ( ( iEdg ‘ 𝐺 ) = ∅ ∧ 𝐺𝑊 ) → 𝐺𝑊 )
9 simpl ( ( ( iEdg ‘ 𝐺 ) = ∅ ∧ 𝐺𝑊 ) → ( iEdg ‘ 𝐺 ) = ∅ )
10 8 9 usgr0e ( ( ( iEdg ‘ 𝐺 ) = ∅ ∧ 𝐺𝑊 ) → 𝐺 ∈ USGraph )
11 10 ex ( ( iEdg ‘ 𝐺 ) = ∅ → ( 𝐺𝑊𝐺 ∈ USGraph ) )
12 7 11 syl6bi ( Fun ( iEdg ‘ 𝐺 ) → ( ran ( iEdg ‘ 𝐺 ) = ∅ → ( 𝐺𝑊𝐺 ∈ USGraph ) ) )
13 12 com13 ( 𝐺𝑊 → ( ran ( iEdg ‘ 𝐺 ) = ∅ → ( Fun ( iEdg ‘ 𝐺 ) → 𝐺 ∈ USGraph ) ) )
14 3 13 sylbid ( 𝐺𝑊 → ( ( Edg ‘ 𝐺 ) = ∅ → ( Fun ( iEdg ‘ 𝐺 ) → 𝐺 ∈ USGraph ) ) )
15 14 3imp ( ( 𝐺𝑊 ∧ ( Edg ‘ 𝐺 ) = ∅ ∧ Fun ( iEdg ‘ 𝐺 ) ) → 𝐺 ∈ USGraph )