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

Metamath Proof Explorer

Theorem cusgr1v

Description: A graph with one vertex and no edges is a complete simple graph. (Contributed by AV, 1-Nov-2020) (Revised by AV, 23-Mar-2021)

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

Proof

Step Hyp Ref Expression
1 cplgr0v.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 cplgr1vlem ⊢ ( ( ♯ ‘ 𝑉 ) = 1 → 𝐺 ∈ V )
3 2 adantr ⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ V )
4 simpr ⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → ( iEdg ‘ 𝐺 ) = ∅ )
5 3 4 usgr0e ⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ USGraph )
6 1 cplgr1v ⊢ ( ( ♯ ‘ 𝑉 ) = 1 → 𝐺 ∈ ComplGraph )
7 6 adantr ⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ ComplGraph )
8 iscusgr ⊢ ( 𝐺 ∈ ComplUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph ) )
9 5 7 8 sylanbrc ⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ ComplUSGraph )