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 )