Theorem usgr1v0edg

Description: A class with one (or no) vertex is a simple graph if and only if it has no edges. (Contributed by Alexander van der Vekens, 13-Oct-2017) (Revised by AV, 18-Oct-2020)

	Ref	Expression
Assertion	usgr1v0edg	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 } ∧ Fun ( iEdg ‘ 𝐺 ) ) → ( 𝐺 ∈ USGraph ↔ ( Edg ‘ 𝐺 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		usgr1v	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 } ) → ( 𝐺 ∈ USGraph ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
2	1	3adant3	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 } ∧ Fun ( iEdg ‘ 𝐺 ) ) → ( 𝐺 ∈ USGraph ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
3		funrel	⊢ ( Fun ( iEdg ‘ 𝐺 ) → Rel ( iEdg ‘ 𝐺 ) )
4		relrn0	⊢ ( Rel ( iEdg ‘ 𝐺 ) → ( ( iEdg ‘ 𝐺 ) = ∅ ↔ ran ( iEdg ‘ 𝐺 ) = ∅ ) )
5	3 4	syl	⊢ ( Fun ( iEdg ‘ 𝐺 ) → ( ( iEdg ‘ 𝐺 ) = ∅ ↔ ran ( iEdg ‘ 𝐺 ) = ∅ ) )
6	5	3ad2ant3	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 } ∧ Fun ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) = ∅ ↔ ran ( iEdg ‘ 𝐺 ) = ∅ ) )
7		edgval	⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
8	7	eqcomi	⊢ ran ( iEdg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
9	8	eqeq1i	⊢ ( ran ( iEdg ‘ 𝐺 ) = ∅ ↔ ( Edg ‘ 𝐺 ) = ∅ )
10	9	a1i	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 } ∧ Fun ( iEdg ‘ 𝐺 ) ) → ( ran ( iEdg ‘ 𝐺 ) = ∅ ↔ ( Edg ‘ 𝐺 ) = ∅ ) )
11	2 6 10	3bitrd	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 } ∧ Fun ( iEdg ‘ 𝐺 ) ) → ( 𝐺 ∈ USGraph ↔ ( Edg ‘ 𝐺 ) = ∅ ) )