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

Metamath Proof Explorer

Theorem uhgr0

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

Ref Expression
Assertion uhgr0 ⊢ ∅ ∈ UHGraph

Proof

Step Hyp Ref Expression
1 f0 ⊢ ∅ : ∅ ⟶ ∅
2 dm0 ⊢ dom ⁡ ∅ = ∅
3 pw0 ⊢ 𝒫 ∅ = ∅
4 3 difeq1i ⊢ 𝒫 ∅ ∖ ∅ = ∅ ∖ ∅
5 difid ⊢ ∅ ∖ ∅ = ∅
6 4 5 eqtri ⊢ 𝒫 ∅ ∖ ∅ = ∅
7 2 6 feq23i ⊢ ∅ : dom ⁡ ∅ ⟶ 𝒫 ∅ ∖ ∅ ↔ ∅ : ∅ ⟶ ∅
8 1 7 mpbir ⊢ ∅ : dom ⁡ ∅ ⟶ 𝒫 ∅ ∖ ∅
9 0ex ⊢ ∅ ∈ V
10 vtxval0 ⊢ Vtx ⁡ ∅ = ∅
11 10 eqcomi ⊢ ∅ = Vtx ⁡ ∅
12 iedgval0 ⊢ iEdg ⁡ ∅ = ∅
13 12 eqcomi ⊢ ∅ = iEdg ⁡ ∅
14 11 13 isuhgr ⊢ ∅ ∈ V → ∅ ∈ UHGraph ↔ ∅ : dom ⁡ ∅ ⟶ 𝒫 ∅ ∖ ∅
15 9 14 ax-mp ⊢ ∅ ∈ UHGraph ↔ ∅ : dom ⁡ ∅ ⟶ 𝒫 ∅ ∖ ∅
16 8 15 mpbir ⊢ ∅ ∈ UHGraph