Metamath Proof Explorer

Theorem uhgr0vb

Description: The null graph, with no vertices, is a hypergraph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 27-Dec-2017) (Revised by AV, 9-Oct-2020)

Ref Expression
Assertion uhgr0vb ⊢G∈W∧Vtx⁡G=∅→G∈UHGraph↔iEdg⁡G=∅

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 eqid ⊢iEdg⁡G=iEdg⁡G
3 1 2 uhgrf ⊢G∈UHGraph→iEdg⁡G:dom⁡iEdg⁡G⟶𝒫Vtx⁡G∖∅
4 pweq ⊢Vtx⁡G=∅→𝒫Vtx⁡G=𝒫∅
5 4 difeq1d ⊢Vtx⁡G=∅→𝒫Vtx⁡G∖∅=𝒫∅∖∅
6 pw0 ⊢𝒫∅=∅
7 6 difeq1i ⊢𝒫∅∖∅=∅∖∅
8 difid ⊢∅∖∅=∅
9 7 8 eqtri ⊢𝒫∅∖∅=∅
10 5 9 eqtrdi ⊢Vtx⁡G=∅→𝒫Vtx⁡G∖∅=∅
11 10 adantl ⊢G∈W∧Vtx⁡G=∅→𝒫Vtx⁡G∖∅=∅
12 11 feq3d ⊢G∈W∧Vtx⁡G=∅→iEdg⁡G:dom⁡iEdg⁡G⟶𝒫Vtx⁡G∖∅↔iEdg⁡G:dom⁡iEdg⁡G⟶∅
13 f00 ⊢iEdg⁡G:dom⁡iEdg⁡G⟶∅↔iEdg⁡G=∅∧dom⁡iEdg⁡G=∅
14 13 simplbi ⊢iEdg⁡G:dom⁡iEdg⁡G⟶∅→iEdg⁡G=∅
15 12 14 syl6bi ⊢G∈W∧Vtx⁡G=∅→iEdg⁡G:dom⁡iEdg⁡G⟶𝒫Vtx⁡G∖∅→iEdg⁡G=∅
16 3 15 syl5 ⊢G∈W∧Vtx⁡G=∅→G∈UHGraph→iEdg⁡G=∅
17 simpl ⊢G∈W∧iEdg⁡G=∅→G∈W
18 simpr ⊢G∈W∧iEdg⁡G=∅→iEdg⁡G=∅
19 17 18 uhgr0e ⊢G∈W∧iEdg⁡G=∅→G∈UHGraph
20 19 ex ⊢G∈W→iEdg⁡G=∅→G∈UHGraph
21 20 adantr ⊢G∈W∧Vtx⁡G=∅→iEdg⁡G=∅→G∈UHGraph
22 16 21 impbid ⊢G∈W∧Vtx⁡G=∅→G∈UHGraph↔iEdg⁡G=∅