Theorem isausgr

Description: The property of an unordered pair to be an alternatively defined simple graph, defined as a pair (V,E) of a set V (vertex set) and a set of unordered pairs of elements of V (edge set). (Contributed by Alexander van der Vekens, 28-Aug-2017)

	Ref	Expression
Hypothesis	ausgr.1	$$⊢G=\left\{⟨v,e⟩|e\subseteq \left\{x\in 𝒫v|\left|x\right|=2\right\}\right\}$$
Assertion	isausgr	$$⊢\left(V\in W\wedge E\in X\right)\to \left(VGE\leftrightarrow E\subseteq \left\{x\in 𝒫V|\left|x\right|=2\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ausgr.1	$$⊢G=\left\{⟨v,e⟩|e\subseteq \left\{x\in 𝒫v|\left|x\right|=2\right\}\right\}$$
2		simpr	$$⊢\left(v=V\wedge e=E\right)\to e=E$$
3		pweq	$$⊢v=V\to 𝒫v=𝒫V$$
4	3	adantr	$$⊢\left(v=V\wedge e=E\right)\to 𝒫v=𝒫V$$
5	4	rabeqdv	$$⊢\left(v=V\wedge e=E\right)\to \left\{x\in 𝒫v|\left|x\right|=2\right\}=\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
6	2 5	sseq12d	$$⊢\left(v=V\wedge e=E\right)\to \left(e\subseteq \left\{x\in 𝒫v|\left|x\right|=2\right\}\leftrightarrow E\subseteq \left\{x\in 𝒫V|\left|x\right|=2\right\}\right)$$
7	6 1	brabga	$$⊢\left(V\in W\wedge E\in X\right)\to \left(VGE\leftrightarrow E\subseteq \left\{x\in 𝒫V|\left|x\right|=2\right\}\right)$$