Metamath Proof Explorer

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 e. CH
Assertion hatomistici 
|- A = ( \/H ` { x e. HAtoms | x C_ A } )

Proof

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