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-1x∈𝒫∅∖∅|x=2
2 dm0 ⊢dom⁡∅=∅
3 f1eq2 ⊢dom⁡∅=∅→∅:dom⁡∅⟶1-1x∈𝒫∅∖∅|x=2↔∅:∅⟶1-1x∈𝒫∅∖∅|x=2
4 2 3 ax-mp ⊢∅:dom⁡∅⟶1-1x∈𝒫∅∖∅|x=2↔∅:∅⟶1-1x∈𝒫∅∖∅|x=2
5 1 4 mpbir ⊢∅:dom⁡∅⟶1-1x∈𝒫∅∖∅|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-1x∈𝒫∅∖∅|x=2
12 6 11 ax-mp ⊢∅∈USGraph↔∅:dom⁡∅⟶1-1x∈𝒫∅∖∅|x=2
13 5 12 mpbir ⊢∅∈USGraph