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 ∈ x b ≤ a ∧ ∀ c ∈ ℝ * ∀ b ∈ x b ≤ c → a ≤ c ↔ ∀ b ∈ x b ≤ a ∧ ∀ c ∈ ℝ * ∀ b ∈ x b ≤ c → a ≤ c
8 4 5 6 7 2 lubdm ⊢ ℝ 𝑠 * ∈ Toset → dom ⁡ lub ⁡ ℝ 𝑠 * = x ∈ 𝒫 ℝ * | ∃! a ∈ ℝ * ∀ b ∈ x b ≤ a ∧ ∀ c ∈ ℝ * ∀ b ∈ x b ≤ c → a ≤ c
9 1 8 ax-mp ⊢ dom ⁡ lub ⁡ ℝ 𝑠 * = x ∈ 𝒫 ℝ * | ∃! a ∈ ℝ * ∀ b ∈ x b ≤ a ∧ ∀ c ∈ ℝ * ∀ b ∈ x b ≤ c → a ≤ c
10 rabid2 ⊢ 𝒫 ℝ * = x ∈ 𝒫 ℝ * | ∃! a ∈ ℝ * ∀ b ∈ x b ≤ a ∧ ∀ c ∈ ℝ * ∀ b ∈ x b ≤ c → a ≤ c ↔ ∀ x ∈ 𝒫 ℝ * ∃! a ∈ ℝ * ∀ b ∈ x b ≤ a ∧ ∀ c ∈ ℝ * ∀ b ∈ x b ≤ 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 ∈ x b < d
15 13 14 supeu ⊢ x ⊆ ℝ * → ∃! a ∈ ℝ * ∀ b ∈ x ¬ a < b ∧ ∀ b ∈ ℝ * b < a → ∃ d ∈ x b < d
16 xrslt ⊢ < = < ℝ 𝑠 *
17 1 a1i ⊢ x ⊆ ℝ * → ℝ 𝑠 * ∈ Toset
18 id ⊢ x ⊆ ℝ * → x ⊆ ℝ *
19 4 16 17 18 5 toslublem ⊢ x ⊆ ℝ * ∧ a ∈ ℝ * → ∀ b ∈ x b ≤ a ∧ ∀ c ∈ ℝ * ∀ b ∈ x b ≤ c → a ≤ c ↔ ∀ b ∈ x ¬ a < b ∧ ∀ b ∈ ℝ * b < a → ∃ d ∈ x b < d
20 19 reubidva ⊢ x ⊆ ℝ * → ∃! a ∈ ℝ * ∀ b ∈ x b ≤ a ∧ ∀ c ∈ ℝ * ∀ b ∈ x b ≤ c → a ≤ c ↔ ∃! a ∈ ℝ * ∀ b ∈ x ¬ a < b ∧ ∀ b ∈ ℝ * b < a → ∃ d ∈ x b < d
21 15 20 mpbird ⊢ x ⊆ ℝ * → ∃! a ∈ ℝ * ∀ b ∈ x b ≤ a ∧ ∀ c ∈ ℝ * ∀ b ∈ x b ≤ c → a ≤ c
22 11 21 sylbi ⊢ x ∈ 𝒫 ℝ * → ∃! a ∈ ℝ * ∀ b ∈ x b ≤ a ∧ ∀ c ∈ ℝ * ∀ b ∈ x b ≤ c → a ≤ c
23 10 22 mprgbir ⊢ 𝒫 ℝ * = x ∈ 𝒫 ℝ * | ∃! a ∈ ℝ * ∀ b ∈ x b ≤ a ∧ ∀ c ∈ ℝ * ∀ b ∈ x b ≤ c → a ≤ c
24 9 23 eqtr4i ⊢ dom ⁡ lub ⁡ ℝ 𝑠 * = 𝒫 ℝ *
25 eqid ⊢ glb ⁡ ℝ 𝑠 * = glb ⁡ ℝ 𝑠 *
26 biid ⊢ ∀ b ∈ x a ≤ b ∧ ∀ c ∈ ℝ * ∀ b ∈ x c ≤ b → c ≤ a ↔ ∀ b ∈ x a ≤ b ∧ ∀ c ∈ ℝ * ∀ b ∈ x c ≤ b → c ≤ a
27 4 5 25 26 2 glbdm ⊢ ℝ 𝑠 * ∈ Toset → dom ⁡ glb ⁡ ℝ 𝑠 * = x ∈ 𝒫 ℝ * | ∃! a ∈ ℝ * ∀ b ∈ x a ≤ b ∧ ∀ c ∈ ℝ * ∀ b ∈ x c ≤ b → c ≤ a
28 1 27 ax-mp ⊢ dom ⁡ glb ⁡ ℝ 𝑠 * = x ∈ 𝒫 ℝ * | ∃! a ∈ ℝ * ∀ b ∈ x a ≤ b ∧ ∀ c ∈ ℝ * ∀ b ∈ x c ≤ b → c ≤ a
29 rabid2 ⊢ 𝒫 ℝ * = x ∈ 𝒫 ℝ * | ∃! a ∈ ℝ * ∀ b ∈ x a ≤ b ∧ ∀ c ∈ ℝ * ∀ b ∈ x c ≤ b → c ≤ a ↔ ∀ x ∈ 𝒫 ℝ * ∃! a ∈ ℝ * ∀ b ∈ x a ≤ b ∧ ∀ c ∈ ℝ * ∀ b ∈ x c ≤ b → c ≤ a
30 cnvso ⊢ < Or ℝ * ↔ < -1 Or ℝ *
31 12 30 mpbi ⊢ < -1 Or ℝ *
32 31 a1i ⊢ x ⊆ ℝ * → < -1 Or ℝ *
33 xrinfmss2 ⊢ x ⊆ ℝ * → ∃ a ∈ ℝ * ∀ b ∈ x ¬ a < -1 b ∧ ∀ b ∈ ℝ * b < -1 a → ∃ d ∈ x b < -1 d
34 32 33 supeu ⊢ x ⊆ ℝ * → ∃! a ∈ ℝ * ∀ b ∈ x ¬ a < -1 b ∧ ∀ b ∈ ℝ * b < -1 a → ∃ d ∈ x b < -1 d
35 4 16 17 18 5 tosglblem ⊢ x ⊆ ℝ * ∧ a ∈ ℝ * → ∀ b ∈ x a ≤ b ∧ ∀ c ∈ ℝ * ∀ b ∈ x c ≤ b → c ≤ a ↔ ∀ b ∈ x ¬ a < -1 b ∧ ∀ b ∈ ℝ * b < -1 a → ∃ d ∈ x b < -1 d
36 35 reubidva ⊢ x ⊆ ℝ * → ∃! a ∈ ℝ * ∀ b ∈ x a ≤ b ∧ ∀ c ∈ ℝ * ∀ b ∈ x c ≤ b → c ≤ a ↔ ∃! a ∈ ℝ * ∀ b ∈ x ¬ a < -1 b ∧ ∀ b ∈ ℝ * b < -1 a → ∃ d ∈ x b < -1 d
37 34 36 mpbird ⊢ x ⊆ ℝ * → ∃! a ∈ ℝ * ∀ b ∈ x a ≤ b ∧ ∀ c ∈ ℝ * ∀ b ∈ x c ≤ b → c ≤ a
38 11 37 sylbi ⊢ x ∈ 𝒫 ℝ * → ∃! a ∈ ℝ * ∀ b ∈ x a ≤ b ∧ ∀ c ∈ ℝ * ∀ b ∈ x c ≤ b → c ≤ a
39 29 38 mprgbir ⊢ 𝒫 ℝ * = x ∈ 𝒫 ℝ * | ∃! a ∈ ℝ * ∀ b ∈ x a ≤ b ∧ ∀ c ∈ ℝ * ∀ b ∈ x c ≤ 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