Theorem unisngl

Description: Taking the union of the set of singletons recovers the initial set. (Contributed by Thierry Arnoux, 9-Jan-2020)

	Ref	Expression
Hypothesis	dissnref.c	$$⊢C=\left\{u|\exists x\in Xu=\left\{x\right\}\right\}$$
Assertion	unisngl	$$⊢X=\bigcup C$$

Proof

Step	Hyp	Ref	Expression
1		dissnref.c	$$⊢C=\left\{u|\exists x\in Xu=\left\{x\right\}\right\}$$
2	1	unieqi	$$⊢\bigcup C=\bigcup \left\{u|\exists x\in Xu=\left\{x\right\}\right\}$$
3		simpl	$$⊢\left(y\in u\wedge u=\left\{x\right\}\right)\to y\in u$$
4		simpr	$$⊢\left(y\in u\wedge u=\left\{x\right\}\right)\to u=\left\{x\right\}$$
5	3 4	eleqtrd	$$⊢\left(y\in u\wedge u=\left\{x\right\}\right)\to y\in \left\{x\right\}$$
6	5	exlimiv	$$⊢\exists u\left(y\in u\wedge u=\left\{x\right\}\right)\to y\in \left\{x\right\}$$
7		eqid	$$⊢\left\{x\right\}=\left\{x\right\}$$
8		snex	$$⊢\left\{x\right\}\in \mathrm{V}$$
9		eleq2	$$⊢u=\left\{x\right\}\to \left(y\in u\leftrightarrow y\in \left\{x\right\}\right)$$
10		eqeq1	$$⊢u=\left\{x\right\}\to \left(u=\left\{x\right\}\leftrightarrow \left\{x\right\}=\left\{x\right\}\right)$$
11	9 10	anbi12d	$$⊢u=\left\{x\right\}\to \left(\left(y\in u\wedge u=\left\{x\right\}\right)\leftrightarrow \left(y\in \left\{x\right\}\wedge \left\{x\right\}=\left\{x\right\}\right)\right)$$
12	8 11	spcev	$$⊢\left(y\in \left\{x\right\}\wedge \left\{x\right\}=\left\{x\right\}\right)\to \exists u\left(y\in u\wedge u=\left\{x\right\}\right)$$
13	7 12	mpan2	$$⊢y\in \left\{x\right\}\to \exists u\left(y\in u\wedge u=\left\{x\right\}\right)$$
14	6 13	impbii	$$⊢\exists u\left(y\in u\wedge u=\left\{x\right\}\right)\leftrightarrow y\in \left\{x\right\}$$
15		velsn	$$⊢y\in \left\{x\right\}\leftrightarrow y=x$$
16		equcom	$$⊢y=x\leftrightarrow x=y$$
17	14 15 16	3bitri	$$⊢\exists u\left(y\in u\wedge u=\left\{x\right\}\right)\leftrightarrow x=y$$
18	17	rexbii	$$⊢\exists x\in X\exists u\left(y\in u\wedge u=\left\{x\right\}\right)\leftrightarrow \exists x\in Xx=y$$
19		r19.42v	$$⊢\exists x\in X\left(y\in u\wedge u=\left\{x\right\}\right)\leftrightarrow \left(y\in u\wedge \exists x\in Xu=\left\{x\right\}\right)$$
20	19	exbii	$$⊢\exists u\exists x\in X\left(y\in u\wedge u=\left\{x\right\}\right)\leftrightarrow \exists u\left(y\in u\wedge \exists x\in Xu=\left\{x\right\}\right)$$
21		rexcom4	$$⊢\exists x\in X\exists u\left(y\in u\wedge u=\left\{x\right\}\right)\leftrightarrow \exists u\exists x\in X\left(y\in u\wedge u=\left\{x\right\}\right)$$
22		eluniab	$$⊢y\in \bigcup \left\{u|\exists x\in Xu=\left\{x\right\}\right\}\leftrightarrow \exists u\left(y\in u\wedge \exists x\in Xu=\left\{x\right\}\right)$$
23	20 21 22	3bitr4ri	$$⊢y\in \bigcup \left\{u|\exists x\in Xu=\left\{x\right\}\right\}\leftrightarrow \exists x\in X\exists u\left(y\in u\wedge u=\left\{x\right\}\right)$$
24		risset	$$⊢y\in X\leftrightarrow \exists x\in Xx=y$$
25	18 23 24	3bitr4i	$$⊢y\in \bigcup \left\{u|\exists x\in Xu=\left\{x\right\}\right\}\leftrightarrow y\in X$$
26	25	eqriv	$$⊢\bigcup \left\{u|\exists x\in Xu=\left\{x\right\}\right\}=X$$
27	2 26	eqtr2i	$$⊢X=\bigcup C$$