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 = ∅