This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iscusgredg

Description: A simple graph is complete iff all vertices are connected by an edge. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 1-Nov-2020)

Ref Expression
Hypotheses iscusgrvtx.v 
|- V = ( Vtx ` G )
iscusgredg.v 
|- E = ( Edg ` G )
Assertion iscusgredg 
|- ( G e. ComplUSGraph <-> ( G e. USGraph /\ A. k e. V A. n e. ( V \ { k } ) { n , k } e. E ) )

Proof

Step Hyp Ref Expression
1 iscusgrvtx.v 
 |-  V = ( Vtx ` G )
2 iscusgredg.v 
 |-  E = ( Edg ` G )
3 iscusgr 
 |-  ( G e. ComplUSGraph <-> ( G e. USGraph /\ G e. ComplGraph ) )
4 1 iscplgrnb 
 |-  ( G e. USGraph -> ( G e. ComplGraph <-> A. k e. V A. n e. ( V \ { k } ) n e. ( G NeighbVtx k ) ) )
5 2 nbusgreledg 
 |-  ( G e. USGraph -> ( n e. ( G NeighbVtx k ) <-> { n , k } e. E ) )
6 5 2ralbidv 
 |-  ( G e. USGraph -> ( A. k e. V A. n e. ( V \ { k } ) n e. ( G NeighbVtx k ) <-> A. k e. V A. n e. ( V \ { k } ) { n , k } e. E ) )
7 4 6 bitrd 
 |-  ( G e. USGraph -> ( G e. ComplGraph <-> A. k e. V A. n e. ( V \ { k } ) { n , k } e. E ) )
8 7 pm5.32i 
 |-  ( ( G e. USGraph /\ G e. ComplGraph ) <-> ( G e. USGraph /\ A. k e. V A. n e. ( V \ { k } ) { n , k } e. E ) )
9 3 8 bitri 
 |-  ( G e. ComplUSGraph <-> ( G e. USGraph /\ A. k e. V A. n e. ( V \ { k } ) { n , k } e. E ) )