This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cusgr0v

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

Ref Expression
Hypothesis cplgr0v.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion cusgr0v ( ( 𝐺 ∈ 𝑊 ∧ 𝑉 = ∅ ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ ComplUSGraph )

Proof

Step Hyp Ref Expression
1 cplgr0v.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 eqeq1i ⊢ ( 𝑉 = ∅ ↔ ( Vtx ‘ 𝐺 ) = ∅ )
3 usgr0v ⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ USGraph )
4 2 3 syl3an2b ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑉 = ∅ ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ USGraph )
5 1 cplgr0v ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑉 = ∅ ) → 𝐺 ∈ ComplGraph )
6 5 3adant3 ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑉 = ∅ ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ ComplGraph )
7 iscusgr ⊢ ( 𝐺 ∈ ComplUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph ) )
8 4 6 7 sylanbrc ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑉 = ∅ ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ ComplUSGraph )