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 ‘ 𝐺 ) = ∅ ) )