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