Metamath Proof Explorer


Theorem usgr1eop

Description: A simple graph with (at least) two different vertices and one edge. If the two vertices were not different, the edge would be a loop. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 18-Oct-2020)

Ref Expression
Assertion usgr1eop V W A X B V C V B C V A B C USGraph

Proof

Step Hyp Ref Expression
1 eqid Vtx V A B C = Vtx V A B C
2 simpllr V W A X B V C V B C A X
3 simplrl V W A X B V C V B C B V
4 simpl V W A X V W
5 4 adantr V W A X B V C V V W
6 snex A B C V
7 6 a1i B C A B C V
8 opvtxfv V W A B C V Vtx V A B C = V
9 5 7 8 syl2an V W A X B V C V B C Vtx V A B C = V
10 3 9 eleqtrrd V W A X B V C V B C B Vtx V A B C
11 simprr V W A X B V C V C V
12 6 a1i B V C V A B C V
13 4 12 8 syl2an V W A X B V C V Vtx V A B C = V
14 11 13 eleqtrrd V W A X B V C V C Vtx V A B C
15 14 adantr V W A X B V C V B C C Vtx V A B C
16 opiedgfv V W A B C V iEdg V A B C = A B C
17 5 7 16 syl2an V W A X B V C V B C iEdg V A B C = A B C
18 simpr V W A X B V C V B C B C
19 1 2 10 15 17 18 usgr1e V W A X B V C V B C V A B C USGraph
20 19 ex V W A X B V C V B C V A B C USGraph