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

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 biimtrdi ⊢ ( 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 )