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 )