Metamath Proof Explorer

Theorem xrsclat

Description: The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018)

Ref Expression
Assertion xrsclat ⊢ℝ𝑠*∈CLat

Proof

Step Hyp Ref Expression
1 xrstos ⊢ℝ𝑠*∈Toset
2 tospos ⊢ℝ𝑠*∈Toset→ℝ𝑠*∈Poset
3 1 2 ax-mp ⊢ℝ𝑠*∈Poset
4 xrsbas ⊢ℝ*=Baseℝ𝑠*
5 xrsle ⊢≤=≤ℝ𝑠*
6 eqid ⊢lub⁡ℝ𝑠*=lub⁡ℝ𝑠*
7 biid ⊢∀b∈xb≤a∧∀c∈ℝ*∀b∈xb≤c→a≤c↔∀b∈xb≤a∧∀c∈ℝ*∀b∈xb≤c→a≤c
8 4 5 6 7 2 lubdm ⊢ℝ𝑠*∈Toset→dom⁡lub⁡ℝ𝑠*=x∈𝒫ℝ*|∃!a∈ℝ*∀b∈xb≤a∧∀c∈ℝ*∀b∈xb≤c→a≤c
9 1 8 ax-mp ⊢dom⁡lub⁡ℝ𝑠*=x∈𝒫ℝ*|∃!a∈ℝ*∀b∈xb≤a∧∀c∈ℝ*∀b∈xb≤c→a≤c
10 rabid2 ⊢𝒫ℝ*=x∈𝒫ℝ*|∃!a∈ℝ*∀b∈xb≤a∧∀c∈ℝ*∀b∈xb≤c→a≤c↔∀x∈𝒫ℝ*∃!a∈ℝ*∀b∈xb≤a∧∀c∈ℝ*∀b∈xb≤c→a≤c
11 velpw ⊢x∈𝒫ℝ*↔x⊆ℝ*
12 xrltso ⊢<Orℝ*
13 12 a1i ⊢x⊆ℝ*→<Orℝ*
14 xrsupss ⊢x⊆ℝ*→∃a∈ℝ*∀b∈x¬a<b∧∀b∈ℝ*b<a→∃d∈xb<d
15 13 14 supeu ⊢x⊆ℝ*→∃!a∈ℝ*∀b∈x¬a<b∧∀b∈ℝ*b<a→∃d∈xb<d
16 xrslt ⊢<=<ℝ𝑠*
17 1 a1i ⊢x⊆ℝ*→ℝ𝑠*∈Toset
18 id ⊢x⊆ℝ*→x⊆ℝ*
19 4 16 17 18 5 toslublem ⊢x⊆ℝ*∧a∈ℝ*→∀b∈xb≤a∧∀c∈ℝ*∀b∈xb≤c→a≤c↔∀b∈x¬a<b∧∀b∈ℝ*b<a→∃d∈xb<d
20 19 reubidva ⊢x⊆ℝ*→∃!a∈ℝ*∀b∈xb≤a∧∀c∈ℝ*∀b∈xb≤c→a≤c↔∃!a∈ℝ*∀b∈x¬a<b∧∀b∈ℝ*b<a→∃d∈xb<d
21 15 20 mpbird ⊢x⊆ℝ*→∃!a∈ℝ*∀b∈xb≤a∧∀c∈ℝ*∀b∈xb≤c→a≤c
22 11 21 sylbi ⊢x∈𝒫ℝ*→∃!a∈ℝ*∀b∈xb≤a∧∀c∈ℝ*∀b∈xb≤c→a≤c
23 10 22 mprgbir ⊢𝒫ℝ*=x∈𝒫ℝ*|∃!a∈ℝ*∀b∈xb≤a∧∀c∈ℝ*∀b∈xb≤c→a≤c
24 9 23 eqtr4i ⊢dom⁡lub⁡ℝ𝑠*=𝒫ℝ*
25 eqid ⊢glb⁡ℝ𝑠*=glb⁡ℝ𝑠*
26 biid ⊢∀b∈xa≤b∧∀c∈ℝ*∀b∈xc≤b→c≤a↔∀b∈xa≤b∧∀c∈ℝ*∀b∈xc≤b→c≤a
27 4 5 25 26 2 glbdm ⊢ℝ𝑠*∈Toset→dom⁡glb⁡ℝ𝑠*=x∈𝒫ℝ*|∃!a∈ℝ*∀b∈xa≤b∧∀c∈ℝ*∀b∈xc≤b→c≤a
28 1 27 ax-mp ⊢dom⁡glb⁡ℝ𝑠*=x∈𝒫ℝ*|∃!a∈ℝ*∀b∈xa≤b∧∀c∈ℝ*∀b∈xc≤b→c≤a
29 rabid2 ⊢𝒫ℝ*=x∈𝒫ℝ*|∃!a∈ℝ*∀b∈xa≤b∧∀c∈ℝ*∀b∈xc≤b→c≤a↔∀x∈𝒫ℝ*∃!a∈ℝ*∀b∈xa≤b∧∀c∈ℝ*∀b∈xc≤b→c≤a
30 cnvso ⊢<Orℝ*↔<-1Orℝ*
31 12 30 mpbi ⊢<-1Orℝ*
32 31 a1i ⊢x⊆ℝ*→<-1Orℝ*
33 xrinfmss2 ⊢x⊆ℝ*→∃a∈ℝ*∀b∈x¬a<-1b∧∀b∈ℝ*b<-1a→∃d∈xb<-1d
34 32 33 supeu ⊢x⊆ℝ*→∃!a∈ℝ*∀b∈x¬a<-1b∧∀b∈ℝ*b<-1a→∃d∈xb<-1d
35 4 16 17 18 5 tosglblem ⊢x⊆ℝ*∧a∈ℝ*→∀b∈xa≤b∧∀c∈ℝ*∀b∈xc≤b→c≤a↔∀b∈x¬a<-1b∧∀b∈ℝ*b<-1a→∃d∈xb<-1d
36 35 reubidva ⊢x⊆ℝ*→∃!a∈ℝ*∀b∈xa≤b∧∀c∈ℝ*∀b∈xc≤b→c≤a↔∃!a∈ℝ*∀b∈x¬a<-1b∧∀b∈ℝ*b<-1a→∃d∈xb<-1d
37 34 36 mpbird ⊢x⊆ℝ*→∃!a∈ℝ*∀b∈xa≤b∧∀c∈ℝ*∀b∈xc≤b→c≤a
38 11 37 sylbi ⊢x∈𝒫ℝ*→∃!a∈ℝ*∀b∈xa≤b∧∀c∈ℝ*∀b∈xc≤b→c≤a
39 29 38 mprgbir ⊢𝒫ℝ*=x∈𝒫ℝ*|∃!a∈ℝ*∀b∈xa≤b∧∀c∈ℝ*∀b∈xc≤b→c≤a
40 28 39 eqtr4i ⊢dom⁡glb⁡ℝ𝑠*=𝒫ℝ*
41 24 40 pm3.2i ⊢dom⁡lub⁡ℝ𝑠*=𝒫ℝ*∧dom⁡glb⁡ℝ𝑠*=𝒫ℝ*
42 4 6 25 isclat ⊢ℝ𝑠*∈CLat↔ℝ𝑠*∈Poset∧dom⁡lub⁡ℝ𝑠*=𝒫ℝ*∧dom⁡glb⁡ℝ𝑠*=𝒫ℝ*
43 3 41 42 mpbir2an ⊢ℝ𝑠*∈CLat