Metamath Proof Explorer

Theorem usgr1v

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 usgr1v ⊢G∈W∧Vtx⁡G=A→G∈USGraph↔iEdg⁡G=∅

Proof

Step Hyp Ref Expression
1 usgr1vr ⊢A∈V∧Vtx⁡G=A→G∈USGraph→iEdg⁡G=∅
2 1 adantrl ⊢A∈V∧G∈W∧Vtx⁡G=A→G∈USGraph→iEdg⁡G=∅
3 simplrl ⊢A∈V∧G∈W∧Vtx⁡G=A∧iEdg⁡G=∅→G∈W
4 simpr ⊢A∈V∧G∈W∧Vtx⁡G=A∧iEdg⁡G=∅→iEdg⁡G=∅
5 3 4 usgr0e ⊢A∈V∧G∈W∧Vtx⁡G=A∧iEdg⁡G=∅→G∈USGraph
6 5 ex ⊢A∈V∧G∈W∧Vtx⁡G=A→iEdg⁡G=∅→G∈USGraph
7 2 6 impbid ⊢A∈V∧G∈W∧Vtx⁡G=A→G∈USGraph↔iEdg⁡G=∅
8 7 ex ⊢A∈V→G∈W∧Vtx⁡G=A→G∈USGraph↔iEdg⁡G=∅
9 snprc ⊢¬A∈V↔A=∅
10 simpl ⊢G∈W∧Vtx⁡G=A→G∈W
11 simprr ⊢A=∅∧G∈W∧Vtx⁡G=A→Vtx⁡G=A
12 simpl ⊢A=∅∧G∈W∧Vtx⁡G=A→A=∅
13 11 12 eqtrd ⊢A=∅∧G∈W∧Vtx⁡G=A→Vtx⁡G=∅
14 usgr0vb ⊢G∈W∧Vtx⁡G=∅→G∈USGraph↔iEdg⁡G=∅
15 10 13 14 syl2an2 ⊢A=∅∧G∈W∧Vtx⁡G=A→G∈USGraph↔iEdg⁡G=∅
16 15 ex ⊢A=∅→G∈W∧Vtx⁡G=A→G∈USGraph↔iEdg⁡G=∅
17 9 16 sylbi ⊢¬A∈V→G∈W∧Vtx⁡G=A→G∈USGraph↔iEdg⁡G=∅
18 8 17 pm2.61i ⊢G∈W∧Vtx⁡G=A→G∈USGraph↔iEdg⁡G=∅