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 ) )