Theorem upgrbi

Description: Show that an unordered pair is a valid edge in a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 28-Feb-2016) (Revised by AV, 28-Feb-2021)

	Ref	Expression
Hypotheses	upgrbi.x	$$⊢X\in V$$
	upgrbi.y	$$⊢Y\in V$$
Assertion	upgrbi	$$⊢\left\{X,Y\right\}\in \left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$

Proof

Step	Hyp	Ref	Expression
1		upgrbi.x	$$⊢X\in V$$
2		upgrbi.y	$$⊢Y\in V$$
3		prssi	$$⊢\left(X\in V\wedge Y\in V\right)\to \left\{X,Y\right\}\subseteq V$$
4	1 2 3	mp2an	$$⊢\left\{X,Y\right\}\subseteq V$$
5		prex	$$⊢\left\{X,Y\right\}\in \mathrm{V}$$
6	5	elpw	$$⊢\left\{X,Y\right\}\in 𝒫V\leftrightarrow \left\{X,Y\right\}\subseteq V$$
7	4 6	mpbir	$$⊢\left\{X,Y\right\}\in 𝒫V$$
8	1	elexi	$$⊢X\in \mathrm{V}$$
9	8	prnz	$$⊢\left\{X,Y\right\}\ne \varnothing$$
10		eldifsn	$$⊢\left\{X,Y\right\}\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)\leftrightarrow \left(\left\{X,Y\right\}\in 𝒫V\wedge \left\{X,Y\right\}\ne \varnothing \right)$$
11	7 9 10	mpbir2an	$$⊢\left\{X,Y\right\}\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)$$
12		hashprlei	$$⊢\left(\left\{X,Y\right\}\in \mathrm{Fin}\wedge \left|\left\{X,Y\right\}\right|\le 2\right)$$
13	12	simpri	$$⊢\left|\left\{X,Y\right\}\right|\le 2$$
14		fveq2	$$⊢x=\left\{X,Y\right\}\to \left|x\right|=\left|\left\{X,Y\right\}\right|$$
15	14	breq1d	$$⊢x=\left\{X,Y\right\}\to \left(\left|x\right|\le 2\leftrightarrow \left|\left\{X,Y\right\}\right|\le 2\right)$$
16	15	elrab	$$⊢\left\{X,Y\right\}\in \left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\leftrightarrow \left(\left\{X,Y\right\}\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)\wedge \left|\left\{X,Y\right\}\right|\le 2\right)$$
17	11 13 16	mpbir2an	$$⊢\left\{X,Y\right\}\in \left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$