Database
GRAPH THEORY
Undirected graphs
Examples for graphs
usgr0e
Metamath Proof Explorer
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 )