Metamath Proof Explorer

Theorem isusgrop

Description: The property of being an undirected simple graph 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, 30-Nov-2020)

		Ref	Expression
	Assertion	isusgrop	$⊢ (V \in W \land E \in X) \to (⟨V, E⟩ \in USGraph \leftrightarrow E : dom E \underset{1-1}{⟶} \{p \in 𝒫 V \| \|p\| = 2\})$

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	isusgrs	$⊢ ⟨V, E⟩ \in V \to (⟨V, E⟩ \in USGraph \leftrightarrow iEdg (⟨V, E⟩) : dom iEdg (⟨V, E⟩) \underset{1-1}{⟶} \{p \in 𝒫 Vtx (⟨V, E⟩) \| \|p\| = 2\})$
5	1 4	mp1i	$⊢ (V \in W \land E \in X) \to (⟨V, E⟩ \in USGraph \leftrightarrow iEdg (⟨V, E⟩) : dom iEdg (⟨V, E⟩) \underset{1-1}{⟶} \{p \in 𝒫 Vtx (⟨V, E⟩) \| \|p\| = 2\})$
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	rabeqdv	$⊢ (V \in W \land E \in X) \to \{p \in 𝒫 Vtx (⟨V, E⟩) \| \|p\| = 2\} = \{p \in 𝒫 V \| \|p\| = 2\}$
11	6 7 10	f1eq123d	$⊢ (V \in W \land E \in X) \to (iEdg (⟨V, E⟩) : dom iEdg (⟨V, E⟩) \underset{1-1}{⟶} \{p \in 𝒫 Vtx (⟨V, E⟩) \| \|p\| = 2\} \leftrightarrow E : dom E \underset{1-1}{⟶} \{p \in 𝒫 V \| \|p\| = 2\})$
12	5 11	bitrd	$⊢ (V \in W \land E \in X) \to (⟨V, E⟩ \in USGraph \leftrightarrow E : dom E \underset{1-1}{⟶} \{p \in 𝒫 V \| \|p\| = 2\})$