isuhgrop

Description: The property of being an undirected hypergraph represented as an ordered pair. The representation as an ordered pair is the usual representation of a graph, see section I.1 of Bollobas p. 1. (Contributed by AV, 1-Jan-2020) (Revised by AV, 9-Oct-2020)

		Ref	Expression
	Assertion	isuhgrop	$⊢ (V \in W \land E \in X) \to (⟨V, E⟩ \in UHGraph \leftrightarrow E : dom E ⟶ 𝒫 V ∖ \{\emptyset\})$

Proof

Step	Hyp	Ref	Expression
1		opex	$⊢ ⟨V, E⟩ \in V$
2		eqid	$⊢ Vtx (⟨V, E⟩) = Vtx (⟨V, E⟩)$
3		eqid	$⊢ iEdg (⟨V, E⟩) = iEdg (⟨V, E⟩)$
4	2 3	isuhgr	$⊢ ⟨V, E⟩ \in V \to (⟨V, E⟩ \in UHGraph \leftrightarrow iEdg (⟨V, E⟩) : dom iEdg (⟨V, E⟩) ⟶ 𝒫 Vtx (⟨V, E⟩) ∖ \{\emptyset\})$
5	1 4	mp1i	$⊢ (V \in W \land E \in X) \to (⟨V, E⟩ \in UHGraph \leftrightarrow iEdg (⟨V, E⟩) : dom iEdg (⟨V, E⟩) ⟶ 𝒫 Vtx (⟨V, E⟩) ∖ \{\emptyset\})$
6		opiedgfv	$⊢ (V \in W \land E \in X) \to iEdg (⟨V, E⟩) = E$
7	6	dmeqd	$⊢ (V \in W \land E \in X) \to dom iEdg (⟨V, E⟩) = dom E$
8		opvtxfv	$⊢ (V \in W \land E \in X) \to Vtx (⟨V, E⟩) = V$
9	8	pweqd	$⊢ (V \in W \land E \in X) \to 𝒫 Vtx (⟨V, E⟩) = 𝒫 V$
10	9	difeq1d	$⊢ (V \in W \land E \in X) \to 𝒫 Vtx (⟨V, E⟩) ∖ \{\emptyset\} = 𝒫 V ∖ \{\emptyset\}$
11	6 7 10	feq123d	$⊢ (V \in W \land E \in X) \to (iEdg (⟨V, E⟩) : dom iEdg (⟨V, E⟩) ⟶ 𝒫 Vtx (⟨V, E⟩) ∖ \{\emptyset\} \leftrightarrow E : dom E ⟶ 𝒫 V ∖ \{\emptyset\})$
12	5 11	bitrd	$⊢ (V \in W \land E \in X) \to (⟨V, E⟩ \in UHGraph \leftrightarrow E : dom E ⟶ 𝒫 V ∖ \{\emptyset\})$

Metamath Proof Explorer

Theorem isuhgrop

Proof