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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | simplr | |
|
3 | simprl | |
|
4 | simpl | |
|
5 | snex | |
|
6 | 5 | a1i | |
7 | opvtxfv | |
|
8 | 4 6 7 | syl2an | |
9 | 3 8 | eleqtrrd | |
10 | simprr | |
|
11 | 10 8 | eleqtrrd | |
12 | opiedgfv | |
|
13 | 4 6 12 | syl2an | |
14 | 1 2 9 11 13 | upgr1e | |