Theorem atpointN

Description: The singleton of an atom is a point. (Contributed by NM, 14-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ispoint.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	ispoint.p	$$⊢P=\mathrm{Points}\left(K\right)$$
Assertion	atpointN	$$⊢\left(K\in D\wedge X\in A\right)\to \left\{X\right\}\in P$$

Proof

Step	Hyp	Ref	Expression
1		ispoint.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		ispoint.p	$$⊢P=\mathrm{Points}\left(K\right)$$
3		eqid	$$⊢\left\{X\right\}=\left\{X\right\}$$
4		sneq	$$⊢x=X\to \left\{x\right\}=\left\{X\right\}$$
5	4	rspceeqv	$$⊢\left(X\in A\wedge \left\{X\right\}=\left\{X\right\}\right)\to \exists x\in A\left\{X\right\}=\left\{x\right\}$$
6	3 5	mpan2	$$⊢X\in A\to \exists x\in A\left\{X\right\}=\left\{x\right\}$$
7	6	adantl	$$⊢\left(K\in D\wedge X\in A\right)\to \exists x\in A\left\{X\right\}=\left\{x\right\}$$
8	1 2	ispointN	$$⊢K\in D\to \left(\left\{X\right\}\in P\leftrightarrow \exists x\in A\left\{X\right\}=\left\{x\right\}\right)$$
9	8	adantr	$$⊢\left(K\in D\wedge X\in A\right)\to \left(\left\{X\right\}\in P\leftrightarrow \exists x\in A\left\{X\right\}=\left\{x\right\}\right)$$
10	7 9	mpbird	$$⊢\left(K\in D\wedge X\in A\right)\to \left\{X\right\}\in P$$