Theorem bj-snmoore

Description: A singleton is a Moore collection. See bj-snmooreb for a biconditional version. (Contributed by BJ, 10-Apr-2024)

	Ref	Expression
Assertion	bj-snmoore	$$⊢A\in V\to \left\{A\right\}\in \underset{\_}{\mathrm{Moore}}$$

Proof

Step	Hyp	Ref	Expression
1		unisng	$$⊢A\in V\to \bigcup \left\{A\right\}=A$$
2		snidg	$$⊢A\in V\to A\in \left\{A\right\}$$
3	1 2	eqeltrd	$$⊢A\in V\to \bigcup \left\{A\right\}\in \left\{A\right\}$$
4		df-ne	$$⊢x\ne \varnothing \leftrightarrow \neg x=\varnothing$$
5		sssn	$$⊢x\subseteq \left\{A\right\}\leftrightarrow \left(x=\varnothing \vee x=\left\{A\right\}\right)$$
6		biorf	$$⊢\neg x=\varnothing \to \left(x=\left\{A\right\}\leftrightarrow \left(x=\varnothing \vee x=\left\{A\right\}\right)\right)$$
7	6	biimpar	$$⊢\left(\neg x=\varnothing \wedge \left(x=\varnothing \vee x=\left\{A\right\}\right)\right)\to x=\left\{A\right\}$$
8	4 5 7	syl2anb	$$⊢\left(x\ne \varnothing \wedge x\subseteq \left\{A\right\}\right)\to x=\left\{A\right\}$$
9		inteq	$$⊢x=\left\{A\right\}\to \bigcap x=\bigcap \left\{A\right\}$$
10		intsng	$$⊢A\in V\to \bigcap \left\{A\right\}=A$$
11		eqtr	$$⊢\left(\bigcap x=\bigcap \left\{A\right\}\wedge \bigcap \left\{A\right\}=A\right)\to \bigcap x=A$$
12	11	ex	$$⊢\bigcap x=\bigcap \left\{A\right\}\to \left(\bigcap \left\{A\right\}=A\to \bigcap x=A\right)$$
13	9 10 12	syl2im	$$⊢x=\left\{A\right\}\to \left(A\in V\to \bigcap x=A\right)$$
14		intex	$$⊢x\ne \varnothing \leftrightarrow \bigcap x\in \mathrm{V}$$
15		elsng	$$⊢\bigcap x\in \mathrm{V}\to \left(\bigcap x\in \left\{A\right\}\leftrightarrow \bigcap x=A\right)$$
16	14 15	sylbi	$$⊢x\ne \varnothing \to \left(\bigcap x\in \left\{A\right\}\leftrightarrow \bigcap x=A\right)$$
17	16	biimprd	$$⊢x\ne \varnothing \to \left(\bigcap x=A\to \bigcap x\in \left\{A\right\}\right)$$
18	13 17	sylan9r	$$⊢\left(x\ne \varnothing \wedge x=\left\{A\right\}\right)\to \left(A\in V\to \bigcap x\in \left\{A\right\}\right)$$
19	8 18	syldan	$$⊢\left(x\ne \varnothing \wedge x\subseteq \left\{A\right\}\right)\to \left(A\in V\to \bigcap x\in \left\{A\right\}\right)$$
20	19	ancoms	$$⊢\left(x\subseteq \left\{A\right\}\wedge x\ne \varnothing \right)\to \left(A\in V\to \bigcap x\in \left\{A\right\}\right)$$
21	20	impcom	$$⊢\left(A\in V\wedge \left(x\subseteq \left\{A\right\}\wedge x\ne \varnothing \right)\right)\to \bigcap x\in \left\{A\right\}$$
22	3 21	bj-ismooredr2	$$⊢A\in V\to \left\{A\right\}\in \underset{\_}{\mathrm{Moore}}$$