Theorem uhgr0vb 26554

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.)

Assertion

Ref	Expression
uhgr0vb	⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → (𝐺 ∈ UHGraph ↔ (iEdg‘𝐺) = ∅))

Proof of Theorem uhgr0vb

Step	Hyp	Ref	Expression
1		eqid 2772	. . . 4 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		eqid 2772	. . . 4 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
3	1, 2	uhgrf 26544	. . 3 ⊢ (𝐺 ∈ UHGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
4		pweq 4419	. . . . . . . 8 ⊢ ((Vtx‘𝐺) = ∅ → 𝒫 (Vtx‘𝐺) = 𝒫 ∅)
5	4	difeq1d 3982	. . . . . . 7 ⊢ ((Vtx‘𝐺) = ∅ → (𝒫 (Vtx‘𝐺) ∖ {∅}) = (𝒫 ∅ ∖ {∅}))
6		pw0 4613	. . . . . . . . 9 ⊢ 𝒫 ∅ = {∅}
7	6	difeq1i 3979	. . . . . . . 8 ⊢ (𝒫 ∅ ∖ {∅}) = ({∅} ∖ {∅})
8		difid 4210	. . . . . . . 8 ⊢ ({∅} ∖ {∅}) = ∅
9	7, 8	eqtri 2796	. . . . . . 7 ⊢ (𝒫 ∅ ∖ {∅}) = ∅
10	5, 9	syl6eq 2824	. . . . . 6 ⊢ ((Vtx‘𝐺) = ∅ → (𝒫 (Vtx‘𝐺) ∖ {∅}) = ∅)
11	10	adantl 474	. . . . 5 ⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → (𝒫 (Vtx‘𝐺) ∖ {∅}) = ∅)
12	11	feq3d 6325	. . . 4 ⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅}) ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶∅))
13		f00 6384	. . . . 5 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶∅ ↔ ((iEdg‘𝐺) = ∅ ∧ dom (iEdg‘𝐺) = ∅))
14	13	simplbi 490	. . . 4 ⊢ ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶∅ → (iEdg‘𝐺) = ∅)
15	12, 14	syl6bi 245	. . 3 ⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖ {∅}) → (iEdg‘𝐺) = ∅))
16	3, 15	syl5 34	. 2 ⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → (𝐺 ∈ UHGraph → (iEdg‘𝐺) = ∅))
17		simpl 475	. . . . 5 ⊢ ((𝐺 ∈ 𝑊 ∧ (iEdg‘𝐺) = ∅) → 𝐺 ∈ 𝑊)
18		simpr 477	. . . . 5 ⊢ ((𝐺 ∈ 𝑊 ∧ (iEdg‘𝐺) = ∅) → (iEdg‘𝐺) = ∅)
19	17, 18	uhgr0e 26553	. . . 4 ⊢ ((𝐺 ∈ 𝑊 ∧ (iEdg‘𝐺) = ∅) → 𝐺 ∈ UHGraph)
20	19	ex 405	. . 3 ⊢ (𝐺 ∈ 𝑊 → ((iEdg‘𝐺) = ∅ → 𝐺 ∈ UHGraph))
21	20	adantr 473	. 2 ⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → ((iEdg‘𝐺) = ∅ → 𝐺 ∈ UHGraph))
22	16, 21	impbid 204	1 ⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → (𝐺 ∈ UHGraph ↔ (iEdg‘𝐺) = ∅))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507   ∈ wcel 2050   ∖ cdif 3820  ∅c0 4172  𝒫 cpw 4416  {csn 4435  dom cdm 5401  ⟶wf 6178  ‘cfv 6182  Vtxcvtx 26478  iEdgciedg 26479  UHGraphcuhgr 26538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-sep 5054  ax-nul 5061  ax-pr 5180

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-sbc 3676  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-br 4924  df-opab 4986  df-id 5306  df-xp 5407  df-rel 5408  df-cnv 5409  df-co 5410  df-dm 5411  df-rn 5412  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-fv 6190  df-uhgr 26540

This theorem is referenced by:  usgr0vb  26716  uhgr0v0e  26717  0uhgrsubgr  26758  finsumvtxdg2size  27029  0uhgrrusgr  27057  frgr0v  27789  frgruhgr0v  27791