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 ⊢ φ → G ∈ W
usgr0e.e ⊢ φ → iEdg ⁡ G = ∅
Assertion usgr0e ⊢ φ → G ∈ USGraph

Proof

Step Hyp Ref Expression
1 usgr0e.g ⊢ φ → G ∈ W
2 usgr0e.e ⊢ φ → iEdg ⁡ G = ∅
3 2 f10d ⊢ φ → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
4 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
5 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
6 4 5 isusgr ⊢ G ∈ W → G ∈ USGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
7 1 6 syl ⊢ φ → G ∈ USGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
8 3 7 mpbird ⊢ φ → G ∈ USGraph