hatomistic - Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
Unicode version

Theorem hatomistic 10289

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 2131	. . . . 5
2		atssch 10270	. . . . 5
3	1, 2	sstri 2073	. . . 4
4		chsupclt 9308	. . . 4 $\/H$
5	3, 4	ax-mp 7	. . 3 $\/H$
6		hatomistic.1	. . . 4
7	6	chshi 9097	. . 3
8		atelch 10271	. . . . . . . 8
9	8	anim1i 334	. . . . . . 7 $/\$ $/\$
10		sseq1 2082	. . . . . . . 8
11	10	elrab 1905	. . . . . . 7 $/\$
12	10	elrab 1905	. . . . . . 7 $/\$
13	9, 11, 12	3imtr4 219	. . . . . 6
14	13	ssriv 2069	. . . . 5
15		ssrab2 2131	. . . . . 6
16		chsupss 9310	. . . . . 6 $/\$ $\/H$ $\/H$
17	3, 15, 16	mp2an 697	. . . . 5 $\/H$ $\/H$
18	14, 17	ax-mp 7	. . . 4 $\/H$ $\/H$
19		chsupid 9311	. . . . 5 $\/H$
20	6, 19	ax-mp 7	. . . 4 $\/H$
21	18, 20	sseqtr 2093	. . 3 $\/H$
22		elssuni 2526	. . . . . . . . . . 11
23	11, 22	sylbir 201	. . . . . . . . . 10 $/\$
24		chsupunss 9316	. . . . . . . . . . . 12 $\/H$
25	3, 24	ax-mp 7	. . . . . . . . . . 11 $\/H$
26		sstr2 2071	. . . . . . . . . . 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 10272	. . . . . . . . . . 11
31	30	adantr 389	. . . . . . . . . 10 $/\$ $\/H$
32		chle0t 9367	. . . . . . . . . . . . . . . 16
33	8, 32	syl 10	. . . . . . . . . . . . . . 15
34		ssin 2232	. . . . . . . . . . . . . . . 16 $\/H$ $/\$ $\/H$ $\/H$ $\/H$
35	5	chocin 9377	. . . . . . . . . . . . . . . . 17 $\/H$ $\/H$
36	35	sseq2i 2086	. . . . . . . . . . . . . . . 16 $\/H$ $\/H$
37	34, 36	bitr2 174	. . . . . . . . . . . . . . 15 $\/H$ $/\$ $\/H$
38	33, 37	syl5bbr 534	. . . . . . . . . . . . . 14 $\/H$ $/\$ $\/H$
39	38	biimpa 416	. . . . . . . . . . . . 13 $/\$ $\/H$ $/\$ $\/H$
40	39	exp32 377	. . . . . . . . . . . 12 $\/H$ $\/H$
41	40	imp 350	. . . . . . . . . . 11 $/\$ $\/H$ $\/H$
42	41	necon3ad 1602	. . . . . . . . . 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 2232	. . . . . . 7 $/\$ $\/H$ $\/H$
49	48	negbii 187	. . . . . 6 $/\$ $\/H$ $\/H$
50	47, 49	sylib 198	. . . . 5 $\/H$
51	50	nrex 1729	. . . 4 $\/H$
52	5	choccl 9185	. . . . . . 7 $\/H$
53	6, 52	chincl 9383	. . . . . 6 $\/H$
54	53	hatomic 10286	. . . . 5 $\/H$ $\/H$
55	54	necon1bi 1609	. . . 4 $\/H$ $\/H$
56	51, 55	ax-mp 7	. . 3 $\/H$
57	5, 7, 21, 56	omlsi 9245	. 2 $\/H$
58	57	eqcomi 1479	1 $\/H$

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3

wb 146 $/\$ wa 223

wceq 956

wcel 958

wne 1585

wrex 1646

crab 1648

cin 2046

wss 2047

cuni 2503

cfv 3182

cch 8798

cort 8799 $\/H$ chsup 8803

c0h 8804

cat 8833

This theorem is referenced by: chpssat 10290

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 962 ax-gen 963 ax-8 964 ax-9 965 ax-10 966 ax-11 967 ax-12 968 ax-13 969 ax-14 970 ax-17 971 ax-4 973 ax-5o 975 ax-6o 978 ax-9o 1123 ax-10o 1140 ax-16 1210 ax-11o 1218 ax-ext 1459 ax-rep 2693 ax-sep 2703 ax-nul 2710 ax-pow 2742 ax-pr 2779 ax-un 2866 ax-reg 4593 ax-inf2 4625 ax-ac 4744 ax-hilex 8869 ax-hfvadd 8870 ax-hvcom 8871 ax-hvass 8872 ax-hv0cl 8873 ax-hvaddid 8874 ax-hfvmul 8875 ax-hvmulid 8876 ax-hvmulass 8877 ax-hvdistr1