Metamath Proof Explorer


Theorem upgr1eop

Description: A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1eop . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 10-Oct-2020)

Ref Expression
Assertion upgr1eop V W A X B V C V V A B C UPGraph

Proof

Step Hyp Ref Expression
1 eqid Vtx V A B C = Vtx V A B C
2 simplr V W A X B V C V A X
3 simprl V W A X B V C V B V
4 simpl V W A X V W
5 snex A B C V
6 5 a1i B V C V A B C V
7 opvtxfv V W A B C V Vtx V A B C = V
8 4 6 7 syl2an V W A X B V C V Vtx V A B C = V
9 3 8 eleqtrrd V W A X B V C V B Vtx V A B C
10 simprr V W A X B V C V C V
11 10 8 eleqtrrd V W A X B V C V C Vtx V A B C
12 opiedgfv V W A B C V iEdg V A B C = A B C
13 4 6 12 syl2an V W A X B V C V iEdg V A B C = A B C
14 1 2 9 11 13 upgr1e V W A X B V C V V A B C UPGraph