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

Metamath Proof Explorer

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 ‘ 𝐺 ) = ∅ ) )