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 biimtrdi ⊢ 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 = ∅