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	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
	uhgr0e.e	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = ∅ )
Assertion	uhgr0e	⊢ ( 𝜑 → 𝐺 ∈ UHGraph )

Proof

Step	Hyp	Ref	Expression
1		uhgr0e.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
2		uhgr0e.e	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = ∅ )
3		f0	⊢ ∅ : ∅ ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } )
4		dm0	⊢ dom ∅ = ∅
5	4	feq2i	⊢ ( ∅ : dom ∅ ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ↔ ∅ : ∅ ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
6	3 5	mpbir	⊢ ∅ : dom ∅ ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } )
7		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
8		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
9	7 8	isuhgr	⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ UHGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) )
10	1 9	syl	⊢ ( 𝜑 → ( 𝐺 ∈ UHGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) )
11		id	⊢ ( ( iEdg ‘ 𝐺 ) = ∅ → ( iEdg ‘ 𝐺 ) = ∅ )
12		dmeq	⊢ ( ( iEdg ‘ 𝐺 ) = ∅ → dom ( iEdg ‘ 𝐺 ) = dom ∅ )
13	11 12	feq12d	⊢ ( ( iEdg ‘ 𝐺 ) = ∅ → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ↔ ∅ : dom ∅ ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) )
14	2 13	syl	⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ↔ ∅ : dom ∅ ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) )
15	10 14	bitrd	⊢ ( 𝜑 → ( 𝐺 ∈ UHGraph ↔ ∅ : dom ∅ ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) )
16	6 15	mpbiri	⊢ ( 𝜑 → 𝐺 ∈ UHGraph )