This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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