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 ⊢ 𝐴 ∈ Cℋ
Assertion hatomistici 𝐴 = ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } )

Proof

Step Hyp Ref Expression
1 hatomistic.1 ⊢ 𝐴 ∈ Cℋ
2 ssrab2 ⊢ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ HAtoms
3 atssch ⊢ HAtoms ⊆ Cℋ
4 2 3 sstri ⊢ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ Cℋ
5 chsupcl ⊢ ( { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ Cℋ → ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ∈ Cℋ )
6 4 5 ax-mp ⊢ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ∈ Cℋ
7 1 chshii ⊢ 𝐴 ∈ Sℋ
8 atelch ⊢ ( 𝑦 ∈ HAtoms → 𝑦 ∈ Cℋ )
9 8 anim1i ⊢ ( ( 𝑦 ∈ HAtoms ∧ 𝑦 ⊆ 𝐴 ) → ( 𝑦 ∈ Cℋ ∧ 𝑦 ⊆ 𝐴 ) )
10 sseq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴 ) )
11 10 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ↔ ( 𝑦 ∈ HAtoms ∧ 𝑦 ⊆ 𝐴 ) )
12 10 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ↔ ( 𝑦 ∈ Cℋ ∧ 𝑦 ⊆ 𝐴 ) )
13 9 11 12 3imtr4i ⊢ ( 𝑦 ∈ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } → 𝑦 ∈ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } )
14 13 ssriv ⊢ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 }
15 ssrab2 ⊢ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ⊆ Cℋ
16 chsupss ⊢ ( ( { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ Cℋ ∧ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ⊆ Cℋ ) → ( { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } → ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ⊆ ( ∨ℋ ‘ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ) ) )
17 4 15 16 mp2an ⊢ ( { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } → ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ⊆ ( ∨ℋ ‘ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ) )
18 14 17 ax-mp ⊢ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ⊆ ( ∨ℋ ‘ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } )
19 chsupid ⊢ ( 𝐴 ∈ Cℋ → ( ∨ℋ ‘ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ) = 𝐴 )
20 1 19 ax-mp ⊢ ( ∨ℋ ‘ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ) = 𝐴
21 18 20 sseqtri ⊢ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ⊆ 𝐴
22 elssuni ⊢ ( 𝑦 ∈ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } → 𝑦 ⊆ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } )
23 11 22 sylbir ⊢ ( ( 𝑦 ∈ HAtoms ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ⊆ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } )
24 chsupunss ⊢ ( { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ Cℋ → ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) )
25 4 24 ax-mp ⊢ ∪ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } )
26 23 25 sstrdi ⊢ ( ( 𝑦 ∈ HAtoms ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ⊆ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) )
27 26 ex ⊢ ( 𝑦 ∈ HAtoms → ( 𝑦 ⊆ 𝐴 → 𝑦 ⊆ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) )
28 atne0 ⊢ ( 𝑦 ∈ HAtoms → 𝑦 ≠ 0ℋ )
29 28 adantr ⊢ ( ( 𝑦 ∈ HAtoms ∧ 𝑦 ⊆ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) → 𝑦 ≠ 0ℋ )
30 ssin ⊢ ( ( 𝑦 ⊆ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ∧ 𝑦 ⊆ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) ↔ 𝑦 ⊆ ( ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ∩ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) )
31 6 chocini ⊢ ( ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ∩ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) = 0ℋ
32 31 sseq2i ⊢ ( 𝑦 ⊆ ( ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ∩ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) ↔ 𝑦 ⊆ 0ℋ )
33 30 32 bitr2i ⊢ ( 𝑦 ⊆ 0ℋ ↔ ( 𝑦 ⊆ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ∧ 𝑦 ⊆ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) )
34 chle0 ⊢ ( 𝑦 ∈ Cℋ → ( 𝑦 ⊆ 0ℋ ↔ 𝑦 = 0ℋ ) )
35 8 34 syl ⊢ ( 𝑦 ∈ HAtoms → ( 𝑦 ⊆ 0ℋ ↔ 𝑦 = 0ℋ ) )
36 33 35 bitr3id ⊢ ( 𝑦 ∈ HAtoms → ( ( 𝑦 ⊆ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ∧ 𝑦 ⊆ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) ↔ 𝑦 = 0ℋ ) )
37 36 biimpa ⊢ ( ( 𝑦 ∈ HAtoms ∧ ( 𝑦 ⊆ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ∧ 𝑦 ⊆ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) ) → 𝑦 = 0ℋ )
38 37 expr ⊢ ( ( 𝑦 ∈ HAtoms ∧ 𝑦 ⊆ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) → ( 𝑦 ⊆ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) → 𝑦 = 0ℋ ) )
39 38 necon3ad ⊢ ( ( 𝑦 ∈ HAtoms ∧ 𝑦 ⊆ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) → ( 𝑦 ≠ 0ℋ → ¬ 𝑦 ⊆ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) )
40 29 39 mpd ⊢ ( ( 𝑦 ∈ HAtoms ∧ 𝑦 ⊆ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) → ¬ 𝑦 ⊆ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) )
41 40 ex ⊢ ( 𝑦 ∈ HAtoms → ( 𝑦 ⊆ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) → ¬ 𝑦 ⊆ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) )
42 27 41 syld ⊢ ( 𝑦 ∈ HAtoms → ( 𝑦 ⊆ 𝐴 → ¬ 𝑦 ⊆ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) )
43 imnan ⊢ ( ( 𝑦 ⊆ 𝐴 → ¬ 𝑦 ⊆ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) ↔ ¬ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ⊆ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) )
44 42 43 sylib ⊢ ( 𝑦 ∈ HAtoms → ¬ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ⊆ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) )
45 ssin ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ⊆ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) ↔ 𝑦 ⊆ ( 𝐴 ∩ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) )
46 44 45 sylnib ⊢ ( 𝑦 ∈ HAtoms → ¬ 𝑦 ⊆ ( 𝐴 ∩ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) )
47 46 nrex ⊢ ¬ ∃ 𝑦 ∈ HAtoms 𝑦 ⊆ ( 𝐴 ∩ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) )
48 6 choccli ⊢ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ∈ Cℋ
49 1 48 chincli ⊢ ( 𝐴 ∩ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) ∈ Cℋ
50 49 hatomici ⊢ ( ( 𝐴 ∩ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) ≠ 0ℋ → ∃ 𝑦 ∈ HAtoms 𝑦 ⊆ ( 𝐴 ∩ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) )
51 50 necon1bi ⊢ ( ¬ ∃ 𝑦 ∈ HAtoms 𝑦 ⊆ ( 𝐴 ∩ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) → ( 𝐴 ∩ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) = 0ℋ )
52 47 51 ax-mp ⊢ ( 𝐴 ∩ ( ⊥ ‘ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) ) = 0ℋ
53 6 7 21 52 omlsii ⊢ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) = 𝐴
54 53 eqcomi ⊢ 𝐴 = ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } )