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→ { 𝑥 ∈ ( 𝒫 ∅ ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
2 dm0 dom ∅ = ∅
3 f1eq2 ( dom ∅ = ∅ → ( ∅ : dom ∅ –1-1→ { 𝑥 ∈ ( 𝒫 ∅ ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ∅ : ∅ –1-1→ { 𝑥 ∈ ( 𝒫 ∅ ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
4 2 3 ax-mp ( ∅ : dom ∅ –1-1→ { 𝑥 ∈ ( 𝒫 ∅ ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ∅ : ∅ –1-1→ { 𝑥 ∈ ( 𝒫 ∅ ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
5 1 4 mpbir ∅ : dom ∅ –1-1→ { 𝑥 ∈ ( 𝒫 ∅ ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 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→ { 𝑥 ∈ ( 𝒫 ∅ ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
12 6 11 ax-mp ( ∅ ∈ USGraph ↔ ∅ : dom ∅ –1-1→ { 𝑥 ∈ ( 𝒫 ∅ ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
13 5 12 mpbir ∅ ∈ USGraph