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