Metamath Proof Explorer


Theorem cplgr2vpr

Description: An undirected hypergraph with two (different) vertices is complete iff there is an edge between these two vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Proof shortened by Alexander van der Vekens, 16-Dec-2017) (Revised by AV, 3-Nov-2020)

Ref Expression
Hypotheses cplgr0v.v V = Vtx G
cplgr2v.e E = Edg G
Assertion cplgr2vpr A X B Y A B G UHGraph V = A B G ComplGraph A B E

Proof

Step Hyp Ref Expression
1 cplgr0v.v V = Vtx G
2 cplgr2v.e E = Edg G
3 simpl G UHGraph V = A B G UHGraph
4 fveq2 V = A B V = A B
5 4 adantl G UHGraph V = A B V = A B
6 elex A X A V
7 elex B Y B V
8 id A B A B
9 hashprb A V B V A B A B = 2
10 9 biimpi A V B V A B A B = 2
11 6 7 8 10 syl3an A X B Y A B A B = 2
12 5 11 sylan9eqr A X B Y A B G UHGraph V = A B V = 2
13 1 2 cplgr2v G UHGraph V = 2 G ComplGraph V E
14 3 12 13 syl2an2 A X B Y A B G UHGraph V = A B G ComplGraph V E
15 simprr A X B Y A B G UHGraph V = A B V = A B
16 15 eleq1d A X B Y A B G UHGraph V = A B V E A B E
17 14 16 bitrd A X B Y A B G UHGraph V = A B G ComplGraph A B E