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 e. W -> ( G e. ComplGraph <-> A. v e. V v e. ( UnivVtx ` G ) ) )

Proof

Step Hyp Ref Expression
1 cplgruvtxb.v 
 |-  V = ( Vtx ` G )
2 1 cplgruvtxb 
 |-  ( G e. W -> ( G e. ComplGraph <-> ( UnivVtx ` G ) = V ) )
3 eqss 
 |-  ( ( UnivVtx ` G ) = V <-> ( ( UnivVtx ` G ) C_ V /\ V C_ ( UnivVtx ` G ) ) )
4 1 uvtxssvtx 
 |-  ( UnivVtx ` G ) C_ V
5 dfss3 
 |-  ( V C_ ( UnivVtx ` G ) <-> A. v e. V v e. ( UnivVtx ` G ) )
6 5 anbi2i 
 |-  ( ( ( UnivVtx ` G ) C_ V /\ V C_ ( UnivVtx ` G ) ) <-> ( ( UnivVtx ` G ) C_ V /\ A. v e. V v e. ( UnivVtx ` G ) ) )
7 4 6 mpbiran 
 |-  ( ( ( UnivVtx ` G ) C_ V /\ V C_ ( UnivVtx ` G ) ) <-> A. v e. V v e. ( UnivVtx ` G ) )
8 3 7 bitri 
 |-  ( ( UnivVtx ` G ) = V <-> A. v e. V v e. ( UnivVtx ` G ) )
9 2 8 bitrdi 
 |-  ( G e. W -> ( G e. ComplGraph <-> A. v e. V v e. ( UnivVtx ` G ) ) )