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 ∈ V → ∀ v ∈ V v ∈ UnivVtx ⁡ G

Proof

Step Hyp Ref Expression
1 cplgruvtxb.v ⊢ V = Vtx ⁡ G
2 fvprc ⊢ ¬ G ∈ V → Vtx ⁡ G = ∅
3 1 eqeq1i ⊢ V = ∅ ↔ Vtx ⁡ G = ∅
4 rzal ⊢ V = ∅ → ∀ v ∈ V v ∈ UnivVtx ⁡ G
5 3 4 sylbir ⊢ Vtx ⁡ G = ∅ → ∀ v ∈ V v ∈ UnivVtx ⁡ G
6 2 5 syl ⊢ ¬ G ∈ V → ∀ v ∈ V v ∈ UnivVtx ⁡ G