Theorem umgr0e

Description: The empty graph, with vertices but no edges, is a multigraph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 25-Nov-2020)

	Ref	Expression
Hypotheses	umgr0e.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
	umgr0e.e	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = ∅ )
Assertion	umgr0e	⊢ ( 𝜑 → 𝐺 ∈ UMGraph )

Proof

Step	Hyp	Ref	Expression
1		umgr0e.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
2		umgr0e.e	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = ∅ )
3	2	f10d	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
4		f1f	⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
5	3 4	syl	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
6		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
7		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
8	6 7	isumgr	⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ UMGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
9	1 8	syl	⊢ ( 𝜑 → ( 𝐺 ∈ UMGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
10	5 9	mpbird	⊢ ( 𝜑 → 𝐺 ∈ UMGraph )