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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	Assertion	prcliscplgr	⊢ ( ¬ 𝐺 ∈ V → ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		cplgruvtxb.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( Vtx ‘ 𝐺 ) = ∅ )
3	1	eqeq1i	⊢ ( 𝑉 = ∅ ↔ ( Vtx ‘ 𝐺 ) = ∅ )
4		rzal	⊢ ( 𝑉 = ∅ → ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) )
5	3 4	sylbir	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) )
6	2 5	syl	⊢ ( ¬ 𝐺 ∈ V → ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) )