hatomistic - Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
Unicode version

Theorem hatomistic 10284

Description:

is atomistic, i.e. any element is the supremum of its atoms. Remark in [Kalmbach] p. 140.

**Hypothesis**
Ref	Expression
hatomistic.1

**Assertion**
Ref	Expression
hatomistic	$\/H$

Distinct variable group:

**Proof of Theorem hatomistic**
Step	Hyp	Ref	Expression
1		ssrab2 2134	. . . . 5
2		atssch 10265	. . . . 5
3	1, 2	sstri 2076	. . . 4
4		chsupclt 9303	. . . 4 $\/H$
5	3, 4	ax-mp 7	. . 3 $\/H$
6		hatomistic.1	. . . 4
7	6	chshi 9092	. . 3
8		atelch 10266	. . . . . . . 8
9	8	anim1i 334	. . . . . . 7 $/\$ $/\$
10		sseq1 2085	. . . . . . . 8
11	10	elrab 1908	. . . . . . 7 $/\$
12	10	elrab 1908	. . . . . . 7 $/\$
13	9, 11, 12	3imtr4 219	. . . . . 6
14	13	ssriv 2072	. . . . 5
15		ssrab2 2134	. . . . . 6
16		chsupss 9305	. . . . . 6 $/\$ $\/H$ $\/H$
17	3, 15, 16	mp2an 699	. . . . 5 $\/H$ $\/H$
18	14, 17	ax-mp 7	. . . 4 $\/H$ $\/H$
19		chsupid 9306	. . . . 5 $\/H$
20	6, 19	ax-mp 7	. . . 4 $\/H$
21	18, 20	sseqtr 2096	. . 3 $\/H$
22		elssuni 2530	. . . . . . . . . . 11
23	11, 22	sylbir 201	. . . . . . . . . 10 $/\$
24		chsupunss 9311	. . . . . . . . . . . 12 $\/H$
25	3, 24	ax-mp 7	. . . . . . . . . . 11 $\/H$
26		sstr2 2074	. . . . . . . . . . 11 $\/H$ $\/H$
27	25, 26	mpi 44	. . . . . . . . . 10 $\/H$
28	23, 27	syl 10	. . . . . . . . 9 $/\$ $\/H$
29	28	ex 373	. . . . . . . 8 $\/H$
30		atn0 10267	. . . . . . . . . . 11
31	30	adantr 391	. . . . . . . . . 10 $/\$ $\/H$
32		chle0t 9362	. . . . . . . . . . . . . . . 16
33	8, 32	syl 10	. . . . . . . . . . . . . . 15
34		ssin 2235	. . . . . . . . . . . . . . . 16 $\/H$ $/\$ $\/H$ $\/H$ $\/H$
35	5	chocin 9372	. . . . . . . . . . . . . . . . 17 $\/H$ $\/H$
36	35	sseq2i 2089	. . . . . . . . . . . . . . . 16 $\/H$ $\/H$
37	34, 36	bitr2 174	. . . . . . . . . . . . . . 15 $\/H$ $/\$ $\/H$
38	33, 37	syl5bbr 536	. . . . . . . . . . . . . 14 $\/H$ $/\$ $\/H$
39	38	biimpa 418	. . . . . . . . . . . . 13 $/\$ $\/H$ $/\$ $\/H$
40	39	exp32 379	. . . . . . . . . . . 12 $\/H$ $\/H$
41	40	imp 350	. . . . . . . . . . 11 $/\$ $\/H$ $\/H$
42	41	necon3ad 1605	. . . . . . . . . 10 $/\$ $\/H$ $\/H$
43	31, 42	mpd 26	. . . . . . . . 9 $/\$ $\/H$ $\/H$
44	43	ex 373	. . . . . . . 8 $\/H$ $\/H$
45	29, 44	syld 27	. . . . . . 7 $\/H$
46		imnan 242	. . . . . . 7 $\/H$ $/\$ $\/H$
47	45, 46	sylib 198	. . . . . 6 $/\$ $\/H$
48		ssin 2235	. . . . . . 7 $/\$ $\/H$ $\/H$
49	48	negbii 187	. . . . . 6 $/\$ $\/H$ $\/H$
50	47, 49	sylib 198	. . . . 5 $\/H$
51	50	nrex 1732	. . . 4 $\/H$
52	5	choccl 9180	. . . . . . 7 $\/H$
53	6, 52	chincl 9378	. . . . . 6 $\/H$
54	53	hatomic 10281	. . . . 5 $\/H$ $\/H$
55	54	necon1bi 1612	. . . 4 $\/H$ $\/H$
56	51, 55	ax-mp 7	. . 3 $\/H$
57	5, 7, 21, 56	omlsi 9240	. 2 $\/H$
58	57	eqcomi 1482	1 $\/H$

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3

wb 146 $/\$ wa 223

wceq 958

wcel 960

wne 1588

wrex 1649

crab 1651

cin 2049

wss 2050

cuni 2507

cfv 3188

cch 8793

cort 8794 $\/H$ chsup 8798

c0h 8799

cat 8828

This theorem is referenced by: chpssat 10285

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 964 ax-gen 965 ax-8 966 ax-9 967 ax-10 968 ax-11 969 ax-12 970 ax-13 971 ax-14 972 ax-17 973 ax-4 975 ax-5o 977 ax-6o 980 ax-9o 1125 ax-10o 1142 ax-16 1212 ax-11o 1220 ax-ext 1462 ax-rep 2698 ax-sep 2708 ax-nul 2715 ax-pow 2748 ax-pr 2785 ax-un 2872 ax-reg 4602 ax-inf2 4634 ax-ac 4754 ax-hilex 8864 ax-hfvadd 8865 ax-hvcom 8866 ax-hvass 8867 ax-hv0cl 8868 ax-hvaddid 8869 ax-hfvmul 8870 ax-hvmulid 8871 ax-hvmulass 8872 ax-hvdistr1