Theorem prcliscplgr

Description: A proper class (representing a null graph, see vtxvalprc ) has the property of a complete graph (see also cplgr0v ), but cannot be an element of ComplGraph , of course. Because of this, a sethood antecedent like G e. W is necessary in the following theorems like iscplgr . (Contributed by AV, 14-Feb-2022)

	Ref	Expression
Hypothesis	cplgruvtxb.v	|- V = ( Vtx ` G )
Assertion	prcliscplgr	|- ( -. G e. _V -> A. v e. V v e. ( UnivVtx ` G ) )

Proof

Step	Hyp	Ref	Expression
1		cplgruvtxb.v	|- V = ( Vtx ` G )
2		fvprc	|- ( -. G e. _V -> ( Vtx ` G ) = (/) )
3	1	eqeq1i	|- ( V = (/) <-> ( Vtx ` G ) = (/) )
4		rzal	|- ( V = (/) -> A. v e. V v e. ( UnivVtx ` G ) )
5	3 4	sylbir	|- ( ( Vtx ` G ) = (/) -> A. v e. V v e. ( UnivVtx ` G ) )
6	2 5	syl	|- ( -. G e. _V -> A. v e. V v e. ( UnivVtx ` G ) )