Metamath Proof Explorer

Theorem usgr0

Description: The null graph represented by an empty set is a simple graph. (Contributed by AV, 16-Oct-2020)

Ref Expression
Assertion usgr0 ⊢ ∅ ∈ USGraph

Proof

Step Hyp Ref Expression
1 f10 ⊢ ∅ : ∅ ⟶ 1-1 x ∈ 𝒫 ∅ ∖ ∅ | x = 2
2 dm0 ⊢ dom ⁡ ∅ = ∅
3 f1eq2 ⊢ dom ⁡ ∅ = ∅ → ∅ : dom ⁡ ∅ ⟶ 1-1 x ∈ 𝒫 ∅ ∖ ∅ | x = 2 ↔ ∅ : ∅ ⟶ 1-1 x ∈ 𝒫 ∅ ∖ ∅ | x = 2
4 2 3 ax-mp ⊢ ∅ : dom ⁡ ∅ ⟶ 1-1 x ∈ 𝒫 ∅ ∖ ∅ | x = 2 ↔ ∅ : ∅ ⟶ 1-1 x ∈ 𝒫 ∅ ∖ ∅ | x = 2
5 1 4 mpbir ⊢ ∅ : dom ⁡ ∅ ⟶ 1-1 x ∈ 𝒫 ∅ ∖ ∅ | x = 2
6 0ex ⊢ ∅ ∈ V
7 vtxval0 ⊢ Vtx ⁡ ∅ = ∅
8 7 eqcomi ⊢ ∅ = Vtx ⁡ ∅
9 iedgval0 ⊢ iEdg ⁡ ∅ = ∅
10 9 eqcomi ⊢ ∅ = iEdg ⁡ ∅
11 8 10 isusgr ⊢ ∅ ∈ V → ∅ ∈ USGraph ↔ ∅ : dom ⁡ ∅ ⟶ 1-1 x ∈ 𝒫 ∅ ∖ ∅ | x = 2
12 6 11 ax-mp ⊢ ∅ ∈ USGraph ↔ ∅ : dom ⁡ ∅ ⟶ 1-1 x ∈ 𝒫 ∅ ∖ ∅ | x = 2
13 5 12 mpbir ⊢ ∅ ∈ USGraph