Theorem en2other2

Description: Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015)

	Ref	Expression
Assertion	en2other2	$$⊢\left(X\in P\wedge P\approx 2_{𝑜}\right)\to \bigcup \left(P\setminus \left\{\bigcup \left(P\setminus \left\{X\right\}\right)\right\}\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		en2eleq	$$⊢\left(X\in P\wedge P\approx 2_{𝑜}\right)\to P=\left\{X,\bigcup \left(P\setminus \left\{X\right\}\right)\right\}$$
2		prcom	$$⊢\left\{X,\bigcup \left(P\setminus \left\{X\right\}\right)\right\}=\left\{\bigcup \left(P\setminus \left\{X\right\}\right),X\right\}$$
3	1 2	eqtrdi	$$⊢\left(X\in P\wedge P\approx 2_{𝑜}\right)\to P=\left\{\bigcup \left(P\setminus \left\{X\right\}\right),X\right\}$$
4	3	difeq1d	$$⊢\left(X\in P\wedge P\approx 2_{𝑜}\right)\to P\setminus \left\{\bigcup \left(P\setminus \left\{X\right\}\right)\right\}=\left\{\bigcup \left(P\setminus \left\{X\right\}\right),X\right\}\setminus \left\{\bigcup \left(P\setminus \left\{X\right\}\right)\right\}$$
5		difprsnss	$$⊢\left\{\bigcup \left(P\setminus \left\{X\right\}\right),X\right\}\setminus \left\{\bigcup \left(P\setminus \left\{X\right\}\right)\right\}\subseteq \left\{X\right\}$$
6	4 5	eqsstrdi	$$⊢\left(X\in P\wedge P\approx 2_{𝑜}\right)\to P\setminus \left\{\bigcup \left(P\setminus \left\{X\right\}\right)\right\}\subseteq \left\{X\right\}$$
7		simpl	$$⊢\left(X\in P\wedge P\approx 2_{𝑜}\right)\to X\in P$$
8		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
9		simpr	$$⊢\left(X\in P\wedge P\approx 2_{𝑜}\right)\to P\approx 2_{𝑜}$$
10		df-2o	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$
11	9 10	breqtrdi	$$⊢\left(X\in P\wedge P\approx 2_{𝑜}\right)\to P\approx \mathrm{suc}{1}_{𝑜}$$
12		dif1ennn	$$⊢\left(1_{𝑜}\in \mathrm{\omega }\wedge P\approx \mathrm{suc}{1}_{𝑜}\wedge X\in P\right)\to \left(P\setminus \left\{X\right\}\right)\approx 1_{𝑜}$$
13	8 11 7 12	mp3an2i	$$⊢\left(X\in P\wedge P\approx 2_{𝑜}\right)\to \left(P\setminus \left\{X\right\}\right)\approx 1_{𝑜}$$
14		en1uniel	$$⊢\left(P\setminus \left\{X\right\}\right)\approx 1_{𝑜}\to \bigcup \left(P\setminus \left\{X\right\}\right)\in \left(P\setminus \left\{X\right\}\right)$$
15		eldifsni	$$⊢\bigcup \left(P\setminus \left\{X\right\}\right)\in \left(P\setminus \left\{X\right\}\right)\to \bigcup \left(P\setminus \left\{X\right\}\right)\ne X$$
16	13 14 15	3syl	$$⊢\left(X\in P\wedge P\approx 2_{𝑜}\right)\to \bigcup \left(P\setminus \left\{X\right\}\right)\ne X$$
17	16	necomd	$$⊢\left(X\in P\wedge P\approx 2_{𝑜}\right)\to X\ne \bigcup \left(P\setminus \left\{X\right\}\right)$$
18		eldifsn	$$⊢X\in \left(P\setminus \left\{\bigcup \left(P\setminus \left\{X\right\}\right)\right\}\right)\leftrightarrow \left(X\in P\wedge X\ne \bigcup \left(P\setminus \left\{X\right\}\right)\right)$$
19	7 17 18	sylanbrc	$$⊢\left(X\in P\wedge P\approx 2_{𝑜}\right)\to X\in \left(P\setminus \left\{\bigcup \left(P\setminus \left\{X\right\}\right)\right\}\right)$$
20	19	snssd	$$⊢\left(X\in P\wedge P\approx 2_{𝑜}\right)\to \left\{X\right\}\subseteq P\setminus \left\{\bigcup \left(P\setminus \left\{X\right\}\right)\right\}$$
21	6 20	eqssd	$$⊢\left(X\in P\wedge P\approx 2_{𝑜}\right)\to P\setminus \left\{\bigcup \left(P\setminus \left\{X\right\}\right)\right\}=\left\{X\right\}$$
22	21	unieqd	$$⊢\left(X\in P\wedge P\approx 2_{𝑜}\right)\to \bigcup \left(P\setminus \left\{\bigcup \left(P\setminus \left\{X\right\}\right)\right\}\right)=\bigcup \left\{X\right\}$$
23		unisng	$$⊢X\in P\to \bigcup \left\{X\right\}=X$$
24	23	adantr	$$⊢\left(X\in P\wedge P\approx 2_{𝑜}\right)\to \bigcup \left\{X\right\}=X$$
25	22 24	eqtrd	$$⊢\left(X\in P\wedge P\approx 2_{𝑜}\right)\to \bigcup \left(P\setminus \left\{\bigcup \left(P\setminus \left\{X\right\}\right)\right\}\right)=X$$