Metamath Proof Explorer


Theorem iscplgr

Description: The property of being a complete graph. (Contributed by AV, 1-Nov-2020)

Ref Expression
Hypothesis cplgruvtxb.v V = Vtx G
Assertion iscplgr G W G ComplGraph v V v UnivVtx G

Proof

Step Hyp Ref Expression
1 cplgruvtxb.v V = Vtx G
2 1 cplgruvtxb G W G ComplGraph UnivVtx G = V
3 eqss UnivVtx G = V UnivVtx G V V UnivVtx G
4 1 uvtxssvtx UnivVtx G V
5 dfss3 V UnivVtx G v V v UnivVtx G
6 5 anbi2i UnivVtx G V V UnivVtx G UnivVtx G V v V v UnivVtx G
7 4 6 mpbiran UnivVtx G V V UnivVtx G v V v UnivVtx G
8 3 7 bitri UnivVtx G = V v V v UnivVtx G
9 2 8 bitrdi G W G ComplGraph v V v UnivVtx G