Theorem iscusgrvtx

Description: A simple graph is complete iff all vertices are uniuversal. (Contributed by AV, 1-Nov-2020)

	Ref	Expression
Hypothesis	iscusgrvtx.v	|- V = ( Vtx ` G )
Assertion	iscusgrvtx	|- ( G e. ComplUSGraph <-> ( G e. USGraph /\ A. v e. V v e. ( UnivVtx ` G ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscusgrvtx.v	|- V = ( Vtx ` G )
2		iscusgr	|- ( G e. ComplUSGraph <-> ( G e. USGraph /\ G e. ComplGraph ) )
3	1	iscplgr	|- ( G e. USGraph -> ( G e. ComplGraph <-> A. v e. V v e. ( UnivVtx ` G ) ) )
4	3	pm5.32i	|- ( ( G e. USGraph /\ G e. ComplGraph ) <-> ( G e. USGraph /\ A. v e. V v e. ( UnivVtx ` G ) ) )
5	2 4	bitri	|- ( G e. ComplUSGraph <-> ( G e. USGraph /\ A. v e. V v e. ( UnivVtx ` G ) ) )