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 VWAXBVCVVABCUPGraph

Proof

Step Hyp Ref Expression
1 eqid VtxVABC=VtxVABC
2 simplr VWAXBVCVAX
3 simprl VWAXBVCVBV
4 simpl VWAXVW
5 snex ABCV
6 5 a1i BVCVABCV
7 opvtxfv VWABCVVtxVABC=V
8 4 6 7 syl2an VWAXBVCVVtxVABC=V
9 3 8 eleqtrrd VWAXBVCVBVtxVABC
10 simprr VWAXBVCVCV
11 10 8 eleqtrrd VWAXBVCVCVtxVABC
12 opiedgfv VWABCViEdgVABC=ABC
13 4 6 12 syl2an VWAXBVCViEdgVABC=ABC
14 1 2 9 11 13 upgr1e VWAXBVCVVABCUPGraph