Metamath Proof Explorer

Theorem uhgr0e

Description: The empty graph, with vertices but no edges, is a hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 25-Nov-2020)

Ref Expression
Hypotheses uhgr0e.g ⊢ φ → G ∈ W
uhgr0e.e ⊢ φ → iEdg ⁡ G = ∅
Assertion uhgr0e ⊢ φ → G ∈ UHGraph

Proof

Step Hyp Ref Expression
1 uhgr0e.g ⊢ φ → G ∈ W
2 uhgr0e.e ⊢ φ → iEdg ⁡ G = ∅
3 f0 ⊢ ∅ : ∅ ⟶ 𝒫 Vtx ⁡ G ∖ ∅
4 dm0 ⊢ dom ⁡ ∅ = ∅
5 4 feq2i ⊢ ∅ : dom ⁡ ∅ ⟶ 𝒫 Vtx ⁡ G ∖ ∅ ↔ ∅ : ∅ ⟶ 𝒫 Vtx ⁡ G ∖ ∅
6 3 5 mpbir ⊢ ∅ : dom ⁡ ∅ ⟶ 𝒫 Vtx ⁡ G ∖ ∅
7 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
8 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
9 7 8 isuhgr ⊢ G ∈ W → G ∈ UHGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 𝒫 Vtx ⁡ G ∖ ∅
10 1 9 syl ⊢ φ → G ∈ UHGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 𝒫 Vtx ⁡ G ∖ ∅
11 id ⊢ iEdg ⁡ G = ∅ → iEdg ⁡ G = ∅
12 dmeq ⊢ iEdg ⁡ G = ∅ → dom ⁡ iEdg ⁡ G = dom ⁡ ∅
13 11 12 feq12d ⊢ iEdg ⁡ G = ∅ → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 𝒫 Vtx ⁡ G ∖ ∅ ↔ ∅ : dom ⁡ ∅ ⟶ 𝒫 Vtx ⁡ G ∖ ∅
14 2 13 syl ⊢ φ → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 𝒫 Vtx ⁡ G ∖ ∅ ↔ ∅ : dom ⁡ ∅ ⟶ 𝒫 Vtx ⁡ G ∖ ∅
15 10 14 bitrd ⊢ φ → G ∈ UHGraph ↔ ∅ : dom ⁡ ∅ ⟶ 𝒫 Vtx ⁡ G ∖ ∅
16 6 15 mpbiri ⊢ φ → G ∈ UHGraph