This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ≤ = ( le ‘ ℝ*𝑠 )
6 eqid ⊢ ( lub ‘ ℝ*𝑠 ) = ( lub ‘ ℝ*𝑠 )
7 biid ⊢ ( ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑎 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐 ) ) ↔ ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑎 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐 ) ) )
8 4 5 6 7 2 lubdm ⊢ ( ℝ*𝑠 ∈ Toset → dom ( lub ‘ ℝ*𝑠 ) = { 𝑥 ∈ 𝒫 ℝ* ∣ ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑎 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐 ) ) } )
9 1 8 ax-mp ⊢ dom ( lub ‘ ℝ*𝑠 ) = { 𝑥 ∈ 𝒫 ℝ* ∣ ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑎 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐 ) ) }
10 rabid2 ⊢ ( 𝒫 ℝ* = { 𝑥 ∈ 𝒫 ℝ* ∣ ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑎 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐 ) ) } ↔ ∀ 𝑥 ∈ 𝒫 ℝ* ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑎 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐 ) ) )
11 velpw ⊢ ( 𝑥 ∈ 𝒫 ℝ* ↔ 𝑥 ⊆ ℝ* )
12 xrltso ⊢ < Or ℝ*
13 12 a1i ⊢ ( 𝑥 ⊆ ℝ* → < Or ℝ* )
14 xrsupss ⊢ ( 𝑥 ⊆ ℝ* → ∃ 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 ¬ 𝑎 < 𝑏 ∧ ∀ 𝑏 ∈ ℝ* ( 𝑏 < 𝑎 → ∃ 𝑑 ∈ 𝑥 𝑏 < 𝑑 ) ) )
15 13 14 supeu ⊢ ( 𝑥 ⊆ ℝ* → ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 ¬ 𝑎 < 𝑏 ∧ ∀ 𝑏 ∈ ℝ* ( 𝑏 < 𝑎 → ∃ 𝑑 ∈ 𝑥 𝑏 < 𝑑 ) ) )
16 xrslt ⊢ < = ( lt ‘ ℝ*𝑠 )
17 1 a1i ⊢ ( 𝑥 ⊆ ℝ* → ℝ*𝑠 ∈ Toset )
18 id ⊢ ( 𝑥 ⊆ ℝ* → 𝑥 ⊆ ℝ* )
19 4 16 17 18 5 toslublem ⊢ ( ( 𝑥 ⊆ ℝ* ∧ 𝑎 ∈ ℝ* ) → ( ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑎 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐 ) ) ↔ ( ∀ 𝑏 ∈ 𝑥 ¬ 𝑎 < 𝑏 ∧ ∀ 𝑏 ∈ ℝ* ( 𝑏 < 𝑎 → ∃ 𝑑 ∈ 𝑥 𝑏 < 𝑑 ) ) ) )
20 19 reubidva ⊢ ( 𝑥 ⊆ ℝ* → ( ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑎 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐 ) ) ↔ ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 ¬ 𝑎 < 𝑏 ∧ ∀ 𝑏 ∈ ℝ* ( 𝑏 < 𝑎 → ∃ 𝑑 ∈ 𝑥 𝑏 < 𝑑 ) ) ) )
21 15 20 mpbird ⊢ ( 𝑥 ⊆ ℝ* → ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑎 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐 ) ) )
22 11 21 sylbi ⊢ ( 𝑥 ∈ 𝒫 ℝ* → ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑎 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐 ) ) )
23 10 22 mprgbir ⊢ 𝒫 ℝ* = { 𝑥 ∈ 𝒫 ℝ* ∣ ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑎 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐 ) ) }
24 9 23 eqtr4i ⊢ dom ( lub ‘ ℝ*𝑠 ) = 𝒫 ℝ*
25 eqid ⊢ ( glb ‘ ℝ*𝑠 ) = ( glb ‘ ℝ*𝑠 )
26 biid ⊢ ( ( ∀ 𝑏 ∈ 𝑥 𝑎 ≤ 𝑏 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎 ) ) ↔ ( ∀ 𝑏 ∈ 𝑥 𝑎 ≤ 𝑏 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎 ) ) )
27 4 5 25 26 2 glbdm ⊢ ( ℝ*𝑠 ∈ Toset → dom ( glb ‘ ℝ*𝑠 ) = { 𝑥 ∈ 𝒫 ℝ* ∣ ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑎 ≤ 𝑏 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎 ) ) } )
28 1 27 ax-mp ⊢ dom ( glb ‘ ℝ*𝑠 ) = { 𝑥 ∈ 𝒫 ℝ* ∣ ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑎 ≤ 𝑏 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎 ) ) }
29 rabid2 ⊢ ( 𝒫 ℝ* = { 𝑥 ∈ 𝒫 ℝ* ∣ ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑎 ≤ 𝑏 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎 ) ) } ↔ ∀ 𝑥 ∈ 𝒫 ℝ* ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑎 ≤ 𝑏 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎 ) ) )
30 cnvso ⊢ ( < Or ℝ* ↔ ◡ < Or ℝ* )
31 12 30 mpbi ⊢ ◡ < Or ℝ*
32 31 a1i ⊢ ( 𝑥 ⊆ ℝ* → ◡ < Or ℝ* )
33 xrinfmss2 ⊢ ( 𝑥 ⊆ ℝ* → ∃ 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 ¬ 𝑎 ◡ < 𝑏 ∧ ∀ 𝑏 ∈ ℝ* ( 𝑏 ◡ < 𝑎 → ∃ 𝑑 ∈ 𝑥 𝑏 ◡ < 𝑑 ) ) )
34 32 33 supeu ⊢ ( 𝑥 ⊆ ℝ* → ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 ¬ 𝑎 ◡ < 𝑏 ∧ ∀ 𝑏 ∈ ℝ* ( 𝑏 ◡ < 𝑎 → ∃ 𝑑 ∈ 𝑥 𝑏 ◡ < 𝑑 ) ) )
35 4 16 17 18 5 tosglblem ⊢ ( ( 𝑥 ⊆ ℝ* ∧ 𝑎 ∈ ℝ* ) → ( ( ∀ 𝑏 ∈ 𝑥 𝑎 ≤ 𝑏 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎 ) ) ↔ ( ∀ 𝑏 ∈ 𝑥 ¬ 𝑎 ◡ < 𝑏 ∧ ∀ 𝑏 ∈ ℝ* ( 𝑏 ◡ < 𝑎 → ∃ 𝑑 ∈ 𝑥 𝑏 ◡ < 𝑑 ) ) ) )
36 35 reubidva ⊢ ( 𝑥 ⊆ ℝ* → ( ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑎 ≤ 𝑏 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎 ) ) ↔ ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 ¬ 𝑎 ◡ < 𝑏 ∧ ∀ 𝑏 ∈ ℝ* ( 𝑏 ◡ < 𝑎 → ∃ 𝑑 ∈ 𝑥 𝑏 ◡ < 𝑑 ) ) ) )
37 34 36 mpbird ⊢ ( 𝑥 ⊆ ℝ* → ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑎 ≤ 𝑏 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎 ) ) )
38 11 37 sylbi ⊢ ( 𝑥 ∈ 𝒫 ℝ* → ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑎 ≤ 𝑏 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎 ) ) )
39 29 38 mprgbir ⊢ 𝒫 ℝ* = { 𝑥 ∈ 𝒫 ℝ* ∣ ∃! 𝑎 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑎 ≤ 𝑏 ∧ ∀ 𝑐 ∈ ℝ* ( ∀ 𝑏 ∈ 𝑥 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎 ) ) }
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