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

Metamath Proof Explorer

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