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

Metamath Proof Explorer

Theorem usgr1vr

Description: A simple graph with one vertex has no edges. (Contributed by AV, 18-Oct-2020) (Revised by AV, 21-Mar-2021) (Proof shortened by AV, 2-Apr-2021)

Ref Expression
Assertion usgr1vr ( ( 𝐴 ∈ 𝑋 ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 } ) → ( 𝐺 ∈ USGraph → ( iEdg ‘ 𝐺 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 usgruhgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
2 1 adantl ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 } ) ∧ 𝐺 ∈ USGraph ) → 𝐺 ∈ UHGraph )
3 fveq2 ⊢ ( ( Vtx ‘ 𝐺 ) = { 𝐴 } → ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = ( ♯ ‘ { 𝐴 } ) )
4 hashsng ⊢ ( 𝐴 ∈ 𝑋 → ( ♯ ‘ { 𝐴 } ) = 1 )
5 3 4 sylan9eqr ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 } ) → ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 1 )
6 5 adantr ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 } ) ∧ 𝐺 ∈ USGraph ) → ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 1 )
7 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
8 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
9 7 8 usgrislfuspgr ⊢ ( 𝐺 ∈ USGraph ↔ ( 𝐺 ∈ USPGraph ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )
10 9 simprbi ⊢ ( 𝐺 ∈ USGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
11 10 adantl ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 } ) ∧ 𝐺 ∈ USGraph ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
12 eqid ⊢ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } = { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) }
13 7 8 12 lfuhgr1v0e ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 1 ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) → ( Edg ‘ 𝐺 ) = ∅ )
14 2 6 11 13 syl3anc ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 } ) ∧ 𝐺 ∈ USGraph ) → ( Edg ‘ 𝐺 ) = ∅ )
15 uhgriedg0edg0 ⊢ ( 𝐺 ∈ UHGraph → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
16 1 15 syl ⊢ ( 𝐺 ∈ USGraph → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
17 16 adantl ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 } ) ∧ 𝐺 ∈ USGraph ) → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
18 14 17 mpbid ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 } ) ∧ 𝐺 ∈ USGraph ) → ( iEdg ‘ 𝐺 ) = ∅ )
19 18 ex ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 } ) → ( 𝐺 ∈ USGraph → ( iEdg ‘ 𝐺 ) = ∅ ) )