Theorem uniintsn

Description: Two ways to express " A is a singleton". See also en1 , en1b , card1 , and eusn . (Contributed by NM, 2-Aug-2010)

	Ref	Expression
Assertion	uniintsn	$$⊢\bigcup A=\bigcap A\leftrightarrow \exists xA=\left\{x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		vn0	$$⊢\mathrm{V}\ne \varnothing$$
2		inteq	$$⊢A=\varnothing \to \bigcap A=\bigcap \varnothing$$
3		int0	$$⊢\bigcap \varnothing =\mathrm{V}$$
4	2 3	eqtrdi	$$⊢A=\varnothing \to \bigcap A=\mathrm{V}$$
5	4	adantl	$$⊢\left(\bigcup A=\bigcap A\wedge A=\varnothing \right)\to \bigcap A=\mathrm{V}$$
6		unieq	$$⊢A=\varnothing \to \bigcup A=\bigcup \varnothing$$
7		uni0	$$⊢\bigcup \varnothing =\varnothing$$
8	6 7	eqtrdi	$$⊢A=\varnothing \to \bigcup A=\varnothing$$
9		eqeq1	$$⊢\bigcup A=\bigcap A\to \left(\bigcup A=\varnothing \leftrightarrow \bigcap A=\varnothing \right)$$
10	8 9	imbitrid	$$⊢\bigcup A=\bigcap A\to \left(A=\varnothing \to \bigcap A=\varnothing \right)$$
11	10	imp	$$⊢\left(\bigcup A=\bigcap A\wedge A=\varnothing \right)\to \bigcap A=\varnothing$$
12	5 11	eqtr3d	$$⊢\left(\bigcup A=\bigcap A\wedge A=\varnothing \right)\to \mathrm{V}=\varnothing$$
13	12	ex	$$⊢\bigcup A=\bigcap A\to \left(A=\varnothing \to \mathrm{V}=\varnothing \right)$$
14	13	necon3d	$$⊢\bigcup A=\bigcap A\to \left(\mathrm{V}\ne \varnothing \to A\ne \varnothing \right)$$
15	1 14	mpi	$$⊢\bigcup A=\bigcap A\to A\ne \varnothing$$
16		n0	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$
17	15 16	sylib	$$⊢\bigcup A=\bigcap A\to \exists xx\in A$$
18		vex	$$⊢x\in \mathrm{V}$$
19		vex	$$⊢y\in \mathrm{V}$$
20	18 19	prss	$$⊢\left(x\in A\wedge y\in A\right)\leftrightarrow \left\{x,y\right\}\subseteq A$$
21		uniss	$$⊢\left\{x,y\right\}\subseteq A\to \bigcup \left\{x,y\right\}\subseteq \bigcup A$$
22	21	adantl	$$⊢\left(\bigcup A=\bigcap A\wedge \left\{x,y\right\}\subseteq A\right)\to \bigcup \left\{x,y\right\}\subseteq \bigcup A$$
23		simpl	$$⊢\left(\bigcup A=\bigcap A\wedge \left\{x,y\right\}\subseteq A\right)\to \bigcup A=\bigcap A$$
24	22 23	sseqtrd	$$⊢\left(\bigcup A=\bigcap A\wedge \left\{x,y\right\}\subseteq A\right)\to \bigcup \left\{x,y\right\}\subseteq \bigcap A$$
25		intss	$$⊢\left\{x,y\right\}\subseteq A\to \bigcap A\subseteq \bigcap \left\{x,y\right\}$$
26	25	adantl	$$⊢\left(\bigcup A=\bigcap A\wedge \left\{x,y\right\}\subseteq A\right)\to \bigcap A\subseteq \bigcap \left\{x,y\right\}$$
27	24 26	sstrd	$$⊢\left(\bigcup A=\bigcap A\wedge \left\{x,y\right\}\subseteq A\right)\to \bigcup \left\{x,y\right\}\subseteq \bigcap \left\{x,y\right\}$$
28	18 19	unipr	$$⊢\bigcup \left\{x,y\right\}=x\cup y$$
29	18 19	intpr	$$⊢\bigcap \left\{x,y\right\}=x\cap y$$
30	27 28 29	3sstr3g	$$⊢\left(\bigcup A=\bigcap A\wedge \left\{x,y\right\}\subseteq A\right)\to x\cup y\subseteq x\cap y$$
31		inss1	$$⊢x\cap y\subseteq x$$
32		ssun1	$$⊢x\subseteq x\cup y$$
33	31 32	sstri	$$⊢x\cap y\subseteq x\cup y$$
34		eqss	$$⊢x\cup y=x\cap y\leftrightarrow \left(x\cup y\subseteq x\cap y\wedge x\cap y\subseteq x\cup y\right)$$
35		uneqin	$$⊢x\cup y=x\cap y\leftrightarrow x=y$$
36	34 35	bitr3i	$$⊢\left(x\cup y\subseteq x\cap y\wedge x\cap y\subseteq x\cup y\right)\leftrightarrow x=y$$
37	30 33 36	sylanblc	$$⊢\left(\bigcup A=\bigcap A\wedge \left\{x,y\right\}\subseteq A\right)\to x=y$$
38	37	ex	$$⊢\bigcup A=\bigcap A\to \left(\left\{x,y\right\}\subseteq A\to x=y\right)$$
39	20 38	biimtrid	$$⊢\bigcup A=\bigcap A\to \left(\left(x\in A\wedge y\in A\right)\to x=y\right)$$
40	39	alrimivv	$$⊢\bigcup A=\bigcap A\to \forall x\forall y\left(\left(x\in A\wedge y\in A\right)\to x=y\right)$$
41	17 40	jca	$$⊢\bigcup A=\bigcap A\to \left(\exists xx\in A\wedge \forall x\forall y\left(\left(x\in A\wedge y\in A\right)\to x=y\right)\right)$$
42		euabsn	$$⊢\exists !xx\in A\leftrightarrow \exists x\left\{x|x\in A\right\}=\left\{x\right\}$$
43		eleq1w	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
44	43	eu4	$$⊢\exists !xx\in A\leftrightarrow \left(\exists xx\in A\wedge \forall x\forall y\left(\left(x\in A\wedge y\in A\right)\to x=y\right)\right)$$
45		abid2	$$⊢\left\{x|x\in A\right\}=A$$
46	45	eqeq1i	$$⊢\left\{x|x\in A\right\}=\left\{x\right\}\leftrightarrow A=\left\{x\right\}$$
47	46	exbii	$$⊢\exists x\left\{x|x\in A\right\}=\left\{x\right\}\leftrightarrow \exists xA=\left\{x\right\}$$
48	42 44 47	3bitr3i	$$⊢\left(\exists xx\in A\wedge \forall x\forall y\left(\left(x\in A\wedge y\in A\right)\to x=y\right)\right)\leftrightarrow \exists xA=\left\{x\right\}$$
49	41 48	sylib	$$⊢\bigcup A=\bigcap A\to \exists xA=\left\{x\right\}$$
50		unisnv	$$⊢\bigcup \left\{x\right\}=x$$
51		unieq	$$⊢A=\left\{x\right\}\to \bigcup A=\bigcup \left\{x\right\}$$
52		inteq	$$⊢A=\left\{x\right\}\to \bigcap A=\bigcap \left\{x\right\}$$
53	18	intsn	$$⊢\bigcap \left\{x\right\}=x$$
54	52 53	eqtrdi	$$⊢A=\left\{x\right\}\to \bigcap A=x$$
55	50 51 54	3eqtr4a	$$⊢A=\left\{x\right\}\to \bigcup A=\bigcap A$$
56	55	exlimiv	$$⊢\exists xA=\left\{x\right\}\to \bigcup A=\bigcap A$$
57	49 56	impbii	$$⊢\bigcup A=\bigcap A\leftrightarrow \exists xA=\left\{x\right\}$$