Theorem hatomistic 10280

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

Hypothesis

Ref	Expression
hatomistic.1	|- A e. CH

Assertion

Ref	Expression
hatomistic	|- A = ( \/H ` {x e. Atoms | x (_ A})

Distinct variable group:   x,A

Proof of Theorem hatomistic

Step	Hyp	Ref	Expression
1		ssrab2 2129	. . . . 5 |- {x e. Atoms | x (_ A} (_ Atoms
2		atssch 10261	. . . . 5 |- Atoms (_ CH
3	1, 2	sstri 2071	. . . 4 |- {x e. Atoms | x (_ A} (_ CH
4		chsupclt 9296	. . . 4 |- ({x e. Atoms | x (_ A} (_ CH -> ( \/H ` {x e. Atoms | x (_ A}) e. CH)
5	3, 4	ax-mp 7	. . 3 |- ( \/H ` {x e. Atoms | x (_ A}) e. CH
6		hatomistic.1	. . . 4 |- A e. CH
7	6	chshi 9085	. . 3 |- A e. SH
8		atelch 10262	. . . . . . . 8 |- (y e. Atoms -> y e. CH)
9	8	anim1i 334	. . . . . . 7 |- ((y e. Atoms /\ y (_ A) -> (y e. CH /\ y (_ A))
10		sseq1 2080	. . . . . . . 8 |- (x = y -> (x (_ A <-> y (_ A))
11	10	elrab 1903	. . . . . . 7 |- (y e. {x e. Atoms | x (_ A} <-> (y e. Atoms /\ y (_ A))
12	10	elrab 1903	. . . . . . 7 |- (y e. {x e. CH | x (_ A} <-> (y e. CH /\ y (_ A))
13	9, 11, 12	3imtr4 219	. . . . . 6 |- (y e. {x e. Atoms | x (_ A} -> y e. {x e. CH | x (_ A})
14	13	ssriv 2067	. . . . 5 |- {x e. Atoms | x (_ A} (_ {x e. CH | x (_ A}
15		ssrab2 2129	. . . . . 6 |- {x e. CH | x (_ A} (_ CH
16		chsupss 9298	. . . . . 6 |- (({x e. Atoms | x (_ A} (_ CH /\ {x e. CH | x (_ A} (_ CH) -> ({x e. Atoms | x (_ A} (_ {x e. CH | x (_ A} -> ( \/H ` {x e. Atoms | x (_ A}) (_ ( \/H ` {x e. CH | x (_ A})))
17	3, 15, 16	mp2an 696	. . . . 5 |- ({x e. Atoms | x (_ A} (_ {x e. CH | x (_ A} -> ( \/H ` {x e. Atoms | x (_ A}) (_ ( \/H ` {x e. CH | x (_ A}))
18	14, 17	ax-mp 7	. . . 4 |- ( \/H ` {x e. Atoms | x (_ A}) (_ ( \/H ` {x e. CH | x (_ A})
19		chsupid 9299	. . . . 5 |- (A e. CH -> ( \/H ` {x e. CH | x (_ A}) = A)
20	6, 19	ax-mp 7	. . . 4 |- ( \/H ` {x e. CH | x (_ A}) = A
21	18, 20	sseqtr 2091	. . 3 |- ( \/H ` {x e. Atoms | x (_ A}) (_ A
22		elssuni 2523	. . . . . . . . . . 11 |- (y e. {x e. Atoms | x (_ A} -> y (_ U.{x e. Atoms | x (_ A})
23	11, 22	sylbir 201	. . . . . . . . . 10 |- ((y e. Atoms /\ y (_ A) -> y (_ U.{x e. Atoms | x (_ A})
24		chsupunss 9304	. . . . . . . . . . . 12 |- ({x e. Atoms | x (_ A} (_ CH -> U.{x e. Atoms | x (_ A} (_ ( \/H ` {x e. Atoms | x (_ A}))
25	3, 24	ax-mp 7	. . . . . . . . . . 11 |- U.{x e. Atoms | x (_ A} (_ ( \/H ` {x e. Atoms | x (_ A})
26		sstr2 2069	. . . . . . . . . . 11 |- (y (_ U.{x e. Atoms | x (_ A} -> (U.{x e. Atoms | x (_ A} (_ ( \/H ` {x e. Atoms | x (_ A}) -> y (_ ( \/H ` {x e. Atoms | x (_ A})))
27	25, 26	mpi 44	. . . . . . . . . 10 |- (y (_ U.{x e. Atoms | x (_ A} -> y (_ ( \/H ` {x e. Atoms | x (_ A}))
28	23, 27	syl 10	. . . . . . . . 9 |- ((y e. Atoms /\ y (_ A) -> y (_ ( \/H ` {x e. Atoms | x (_ A}))
29	28	ex 373	. . . . . . . 8 |- (y e. Atoms -> (y (_ A -> y (_ ( \/H ` {x e. Atoms | x (_ A})))
30		atn0 10263	. . . . . . . . . . 11 |- (y e. Atoms -> y =/= 0H)
31	30	adantr 389	. . . . . . . . . 10 |- ((y e. Atoms /\ y (_ ( \/H ` {x e. Atoms | x (_ A})) -> y =/= 0H)
32		chle0t 9355	. . . . . . . . . . . . . . . 16 |- (y e. CH -> (y (_ 0H <-> y = 0H))
33	8, 32	syl 10	. . . . . . . . . . . . . . 15 |- (y e. Atoms -> (y (_ 0H <-> y = 0H))
34		ssin 2230	. . . . . . . . . . . . . . . 16 |- ((y (_ ( \/H ` {x e. Atoms | x (_ A}) /\ y (_ (_|_` ( \/H ` {x e. Atoms | x (_ A}))) <-> y (_ (( \/H ` {x e. Atoms | x (_ A}) i^i (_|_` ( \/H ` {x e. Atoms | x (_ A}))))
35	5	chocin 9365	. . . . . . . . . . . . . . . . 17 |- (( \/H ` {x e. Atoms | x (_ A}) i^i (_|_` ( \/H ` {x e. Atoms | x (_ A}))) = 0H
36	35	sseq2i 2084	. . . . . . . . . . . . . . . 16 |- (y (_ (( \/H ` {x e. Atoms | x (_ A}) i^i (_|_` ( \/H ` {x e. Atoms | x (_ A}))) <-> y (_ 0H)
37	34, 36	bitr2 174	. . . . . . . . . . . . . . 15 |- (y (_ 0H <-> (y (_ ( \/H ` {x e. Atoms | x (_ A}) /\ y (_ (_|_` ( \/H ` {x e. Atoms | x (_ A}))))
38	33, 37	syl5bbr 533	. . . . . . . . . . . . . 14 |- (y e. Atoms -> ((y (_ ( \/H ` {x e. Atoms | x (_ A}) /\ y (_ (_|_` ( \/H ` {x e. Atoms | x (_ A}))) <-> y = 0H))
39	38	biimpa 416	. . . . . . . . . . . . 13 |- ((y e. Atoms /\ (y (_ ( \/H ` {x e. Atoms | x (_ A}) /\ y (_ (_|_` ( \/H ` {x e. Atoms | x (_ A})))) -> y = 0H)
40	39	exp32 377	. . . . . . . . . . . 12 |- (y e. Atoms -> (y (_ ( \/H ` {x e. Atoms | x (_ A}) -> (y (_ (_|_` ( \/H ` {x e. Atoms | x (_ A})) -> y = 0H)))
41	40	imp 350	. . . . . . . . . . 11 |- ((y e. Atoms /\ y (_ ( \/H ` {x e. Atoms | x (_ A})) -> (y (_ (_|_` ( \/H ` {x e. Atoms | x (_ A})) -> y = 0H))
42	41	necon3ad 1601	. . . . . . . . . 10 |- ((y e. Atoms /\ y (_ ( \/H ` {x e. Atoms | x (_ A})) -> (y =/= 0H -> -. y (_ (_|_` ( \/H ` {x e. Atoms | x (_ A}))))
43	31, 42	mpd 26	. . . . . . . . 9 |- ((y e. Atoms /\ y (_ ( \/H ` {x e. Atoms | x (_ A})) -> -. y (_ (_|_` ( \/H ` {x e. Atoms | x (_ A})))
44	43	ex 373	. . . . . . . 8 |- (y e. Atoms -> (y (_ ( \/H ` {x e. Atoms | x (_ A}) -> -. y (_ (_|_` ( \/H ` {x e. Atoms | x (_ A}))))
45	29, 44	syld 27	. . . . . . 7 |- (y e. Atoms -> (y (_ A -> -. y (_ (_|_` ( \/H ` {x e. Atoms | x (_ A}))))
46		imnan 242	. . . . . . 7 |- ((y (_ A -> -. y (_ (_|_` ( \/H ` {x e. Atoms | x (_ A}))) <-> -. (y (_ A /\ y (_ (_|_` ( \/H ` {x e. Atoms | x (_ A}))))
47	45, 46	sylib 198	. . . . . 6 |- (y e. Atoms -> -. (y (_ A /\ y (_ (_|_` ( \/H ` {x e. Atoms | x (_ A}))))
48		ssin 2230	. . . . . . 7 |- ((y (_ A /\ y (_ (_|_` ( \/H ` {x e. Atoms | x (_ A}))) <-> y (_ (A i^i (_|_` ( \/H ` {x e. Atoms | x (_ A}))))
49	48	negbii 187	. . . . . 6 |- (-. (y (_ A /\ y (_ (_|_` ( \/H ` {x e. Atoms | x (_ A}))) <-> -. y (_ (A i^i (_|_` ( \/H ` {x e. Atoms | x (_ A}))))
50	47, 49	sylib 198	. . . . 5 |- (y e. Atoms -> -. y (_ (A i^i (_|_` ( \/H ` {x e. Atoms | x (_ A}))))
51	50	nrex 1728	. . . 4 |- -. E.y e. Atoms y (_ (A i^i (_|_` ( \/H ` {x e. Atoms | x (_ A})))
52	5	choccl 9173	. . . . . . 7 |- (_|_` ( \/H ` {x e. Atoms | x (_ A})) e. CH
53	6, 52	chincl 9371	. . . . . 6 |- (A i^i (_|_` ( \/H ` {x e. Atoms | x (_ A}))) e. CH
54	53	hatomic 10277	. . . . 5 |- ((A i^i (_|_` ( \/H ` {x e. Atoms | x (_ A}))) =/= 0H -> E.y e. Atoms y (_ (A i^i (_|_` ( \/H ` {x e. Atoms | x (_ A}))))
55	54	necon1bi 1608	. . . 4 |- (-. E.y e. Atoms y (_ (A i^i (_|_` ( \/H ` {x e. Atoms | x (_ A}))) -> (A i^i (_|_` ( \/H ` {x e. Atoms | x (_ A}))) = 0H)
56	51, 55	ax-mp 7	. . 3 |- (A i^i (_|_` ( \/H ` {x e. Atoms | x (_ A}))) = 0H
57	5, 7, 21, 56	omlsi 9233	. 2 |- ( \/H ` {x e. Atoms | x (_ A}) = A
58	57	eqcomi 1478	1 |- A = ( \/H ` {x e. Atoms | x (_ A})

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223   = wceq 955   e. wcel 957   =/= wne 1584  E.wrex 1645  {crab 1647   i^i cin 2044   (_ wss 2045  U.cuni 2500  ` cfv 3179  CHcch 8782  _|_cort 8783   \/H chsup 8787  0Hc0h 8788  Atomscat 8817

This theorem is referenced by:  chpssat 10281

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2690  ax-sep 2700  ax-nul 2707  ax-pow 2739  ax-pr 2776  ax-un 2863  ax-reg 4580  ax-inf2 4612  ax-ac 4731  ax-hilex 8853  ax-hfvadd 8854  ax-hvcom 8855  ax-hvass 8856  ax-hv0cl 8857  ax-hvaddid 8858  ax-hfvmul 8859  ax-hvmulid 8860  ax-hvmulass 8861  ax-hvdistr1