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 𝑉 = ( Vtx ‘ 𝐺 )
Assertion cplgr0v ( ( 𝐺𝑊𝑉 = ∅ ) → 𝐺 ∈ ComplGraph )

Proof

Step Hyp Ref Expression
1 cplgr0v.v 𝑉 = ( Vtx ‘ 𝐺 )
2 rzal ( 𝑉 = ∅ → ∀ 𝑣𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) )
3 2 adantl ( ( 𝐺𝑊𝑉 = ∅ ) → ∀ 𝑣𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) )
4 1 iscplgr ( 𝐺𝑊 → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑣𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ) )
5 4 adantr ( ( 𝐺𝑊𝑉 = ∅ ) → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑣𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ) )
6 3 5 mpbird ( ( 𝐺𝑊𝑉 = ∅ ) → 𝐺 ∈ ComplGraph )