Metamath Proof Explorer


Theorem usgr0e

Description: The empty graph, with vertices but no edges, is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020) (Proof shortened by AV, 25-Nov-2020)

Ref Expression
Hypotheses usgr0e.g ( 𝜑𝐺𝑊 )
usgr0e.e ( 𝜑 → ( iEdg ‘ 𝐺 ) = ∅ )
Assertion usgr0e ( 𝜑𝐺 ∈ USGraph )

Proof

Step Hyp Ref Expression
1 usgr0e.g ( 𝜑𝐺𝑊 )
2 usgr0e.e ( 𝜑 → ( iEdg ‘ 𝐺 ) = ∅ )
3 2 f10d ( 𝜑 → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
4 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
6 4 5 isusgr ( 𝐺𝑊 → ( 𝐺 ∈ USGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
7 1 6 syl ( 𝜑 → ( 𝐺 ∈ USGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
8 3 7 mpbird ( 𝜑𝐺 ∈ USGraph )