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	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ UHGraph ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )

Proof

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