Theorem hatomistici

Description: CH is atomistic, i.e. any element is the supremum of its atoms. Remark in Kalmbach p. 140. (Contributed by NM, 14-Aug-2002) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hatomistic.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	hatomistici	$$⊢A={\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		hatomistic.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		ssrab2	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq \mathrm{HAtoms}$$
3		atssch	$$⊢\mathrm{HAtoms}\subseteq {\mathbf{C}}_{\mathscr{H}}$$
4	2 3	sstri	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}$$
5		chsupcl	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}\to {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
6	4 5	ax-mp	$$⊢{\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
7	1	chshii	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
8		atelch	$$⊢y\in \mathrm{HAtoms}\to y\in {\mathbf{C}}_{\mathscr{H}}$$
9	8	anim1i	$$⊢\left(y\in \mathrm{HAtoms}\wedge y\subseteq A\right)\to \left(y\in {\mathbf{C}}_{\mathscr{H}}\wedge y\subseteq A\right)$$
10		sseq1	$$⊢x=y\to \left(x\subseteq A\leftrightarrow y\subseteq A\right)$$
11	10	elrab	$$⊢y\in \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\leftrightarrow \left(y\in \mathrm{HAtoms}\wedge y\subseteq A\right)$$
12	10	elrab	$$⊢y\in \left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\leftrightarrow \left(y\in {\mathbf{C}}_{\mathscr{H}}\wedge y\subseteq A\right)$$
13	9 11 12	3imtr4i	$$⊢y\in \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\to y\in \left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}$$
14	13	ssriv	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq \left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}$$
15		ssrab2	$$⊢\left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}$$
16		chsupss	$$⊢\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge \left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq \left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\to {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\right)\right)$$
17	4 15 16	mp2an	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq \left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\to {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\right)$$
18	14 17	ax-mp	$$⊢{\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\right)$$
19		chsupid	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to {\bigvee }_{\mathscr{H}}\left(\left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\right)=A$$
20	1 19	ax-mp	$$⊢{\bigvee }_{\mathscr{H}}\left(\left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\right)=A$$
21	18 20	sseqtri	$$⊢{\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\subseteq A$$
22		elssuni	$$⊢y\in \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\to y\subseteq \bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}$$
23	11 22	sylbir	$$⊢\left(y\in \mathrm{HAtoms}\wedge y\subseteq A\right)\to y\subseteq \bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}$$
24		chsupunss	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}\to \bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$
25	4 24	ax-mp	$$⊢\bigcup \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$
26	23 25	sstrdi	$$⊢\left(y\in \mathrm{HAtoms}\wedge y\subseteq A\right)\to y\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$
27	26	ex	$$⊢y\in \mathrm{HAtoms}\to \left(y\subseteq A\to y\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)$$
28		atne0	$$⊢y\in \mathrm{HAtoms}\to y\ne 0_{\mathscr{H}}$$
29	28	adantr	$$⊢\left(y\in \mathrm{HAtoms}\wedge y\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\to y\ne 0_{\mathscr{H}}$$
30		ssin	$$⊢\left(y\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\wedge y\subseteq \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\right)\leftrightarrow y\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\cap \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)$$
31	6	chocini	$$⊢{\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\cap \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)=0_{\mathscr{H}}$$
32	31	sseq2i	$$⊢y\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\cap \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\leftrightarrow y\subseteq 0_{\mathscr{H}}$$
33	30 32	bitr2i	$$⊢y\subseteq 0_{\mathscr{H}}\leftrightarrow \left(y\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\wedge y\subseteq \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\right)$$
34		chle0	$$⊢y\in {\mathbf{C}}_{\mathscr{H}}\to \left(y\subseteq 0_{\mathscr{H}}\leftrightarrow y=0_{\mathscr{H}}\right)$$
35	8 34	syl	$$⊢y\in \mathrm{HAtoms}\to \left(y\subseteq 0_{\mathscr{H}}\leftrightarrow y=0_{\mathscr{H}}\right)$$
36	33 35	bitr3id	$$⊢y\in \mathrm{HAtoms}\to \left(\left(y\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\wedge y\subseteq \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\right)\leftrightarrow y=0_{\mathscr{H}}\right)$$
37	36	biimpa	$$⊢\left(y\in \mathrm{HAtoms}\wedge \left(y\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\wedge y\subseteq \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\right)\right)\to y=0_{\mathscr{H}}$$
38	37	expr	$$⊢\left(y\in \mathrm{HAtoms}\wedge y\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\to \left(y\subseteq \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\to y=0_{\mathscr{H}}\right)$$
39	38	necon3ad	$$⊢\left(y\in \mathrm{HAtoms}\wedge y\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\to \left(y\ne 0_{\mathscr{H}}\to \neg y\subseteq \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\right)$$
40	29 39	mpd	$$⊢\left(y\in \mathrm{HAtoms}\wedge y\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\to \neg y\subseteq \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)$$
41	40	ex	$$⊢y\in \mathrm{HAtoms}\to \left(y\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\to \neg y\subseteq \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\right)$$
42	27 41	syld	$$⊢y\in \mathrm{HAtoms}\to \left(y\subseteq A\to \neg y\subseteq \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\right)$$
43		imnan	$$⊢\left(y\subseteq A\to \neg y\subseteq \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\right)\leftrightarrow \neg \left(y\subseteq A\wedge y\subseteq \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\right)$$
44	42 43	sylib	$$⊢y\in \mathrm{HAtoms}\to \neg \left(y\subseteq A\wedge y\subseteq \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\right)$$
45		ssin	$$⊢\left(y\subseteq A\wedge y\subseteq \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\right)\leftrightarrow y\subseteq A\cap \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)$$
46	44 45	sylnib	$$⊢y\in \mathrm{HAtoms}\to \neg y\subseteq A\cap \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)$$
47	46	nrex	$$⊢\neg \exists y\in \mathrm{HAtoms}y\subseteq A\cap \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)$$
48	6	choccli	$$⊢\perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\in {\mathbf{C}}_{\mathscr{H}}$$
49	1 48	chincli	$$⊢A\cap \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\in {\mathbf{C}}_{\mathscr{H}}$$
50	49	hatomici	$$⊢A\cap \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\ne 0_{\mathscr{H}}\to \exists y\in \mathrm{HAtoms}y\subseteq A\cap \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)$$
51	50	necon1bi	$$⊢\neg \exists y\in \mathrm{HAtoms}y\subseteq A\cap \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)\to A\cap \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)=0_{\mathscr{H}}$$
52	47 51	ax-mp	$$⊢A\cap \perp \left({\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)=0_{\mathscr{H}}$$
53	6 7 21 52	omlsii	$$⊢{\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)=A$$
54	53	eqcomi	$$⊢A={\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$