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 =