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