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 C_{ℋ}$
	Assertion	hatomistici	$⊢ A = ⋁_{ℋ} (\{x \in HAtoms \| x \subseteq A\})$

Proof

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

Metamath Proof Explorer

Theorem hatomistici

Proof