Metamath Proof Explorer

Theorem cplgr0v

Description: A null graph (with no vertices) is a complete graph. (Contributed by Alexander van der Vekens, 13-Oct-2017) (Revised by AV, 1-Nov-2020)

Ref Expression
Hypothesis cplgr0v.v ⊢ V = Vtx ⁡ G
Assertion cplgr0v ⊢ G ∈ W ∧ V = ∅ → G ∈ ComplGraph

Proof

Step Hyp Ref Expression
1 cplgr0v.v ⊢ V = Vtx ⁡ G
2 rzal ⊢ V = ∅ → ∀ v ∈ V v ∈ UnivVtx ⁡ G
3 2 adantl ⊢ G ∈ W ∧ V = ∅ → ∀ v ∈ V v ∈ UnivVtx ⁡ G
4 1 iscplgr ⊢ G ∈ W → G ∈ ComplGraph ↔ ∀ v ∈ V v ∈ UnivVtx ⁡ G
5 4 adantr ⊢ G ∈ W ∧ V = ∅ → G ∈ ComplGraph ↔ ∀ v ∈ V v ∈ UnivVtx ⁡ G
6 3 5 mpbird ⊢ G ∈ W ∧ V = ∅ → G ∈ ComplGraph