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 
|- RR*s e. CLat

Proof

Step Hyp Ref Expression
1 xrstos 
 |-  RR*s e. Toset
2 tospos 
 |-  ( RR*s e. Toset -> RR*s e. Poset )
3 1 2 ax-mp 
 |-  RR*s e. Poset
4 xrsbas 
 |-  RR* = ( Base ` RR*s )
5 xrsle 
 |-  <_ = ( le ` RR*s )
6 eqid 
 |-  ( lub ` RR*s ) = ( lub ` RR*s )
7 biid 
 |-  ( ( A. b e. x b <_ a /\ A. c e. RR* ( A. b e. x b <_ c -> a <_ c ) ) <-> ( A. b e. x b <_ a /\ A. c e. RR* ( A. b e. x b <_ c -> a <_ c ) ) )
8 4 5 6 7 2 lubdm 
 |-  ( RR*s e. Toset -> dom ( lub ` RR*s ) = { x e. ~P RR* | E! a e. RR* ( A. b e. x b <_ a /\ A. c e. RR* ( A. b e. x b <_ c -> a <_ c ) ) } )
9 1 8 ax-mp 
 |-  dom ( lub ` RR*s ) = { x e. ~P RR* | E! a e. RR* ( A. b e. x b <_ a /\ A. c e. RR* ( A. b e. x b <_ c -> a <_ c ) ) }
10 rabid2 
 |-  ( ~P RR* = { x e. ~P RR* | E! a e. RR* ( A. b e. x b <_ a /\ A. c e. RR* ( A. b e. x b <_ c -> a <_ c ) ) } <-> A. x e. ~P RR* E! a e. RR* ( A. b e. x b <_ a /\ A. c e. RR* ( A. b e. x b <_ c -> a <_ c ) ) )
11 velpw 
 |-  ( x e. ~P RR* <-> x C_ RR* )
12 xrltso 
 |-  < Or RR*
13 12 a1i 
 |-  ( x C_ RR* -> < Or RR* )
14 xrsupss 
 |-  ( x C_ RR* -> E. a e. RR* ( A. b e. x -. a < b /\ A. b e. RR* ( b < a -> E. d e. x b < d ) ) )
15 13 14 supeu 
 |-  ( x C_ RR* -> E! a e. RR* ( A. b e. x -. a < b /\ A. b e. RR* ( b < a -> E. d e. x b < d ) ) )
16 xrslt 
 |-  < = ( lt ` RR*s )
17 1 a1i 
 |-  ( x C_ RR* -> RR*s e. Toset )
18 id 
 |-  ( x C_ RR* -> x C_ RR* )
19 4 16 17 18 5 toslublem 
 |-  ( ( x C_ RR* /\ a e. RR* ) -> ( ( A. b e. x b <_ a /\ A. c e. RR* ( A. b e. x b <_ c -> a <_ c ) ) <-> ( A. b e. x -. a < b /\ A. b e. RR* ( b < a -> E. d e. x b < d ) ) ) )
20 19 reubidva 
 |-  ( x C_ RR* -> ( E! a e. RR* ( A. b e. x b <_ a /\ A. c e. RR* ( A. b e. x b <_ c -> a <_ c ) ) <-> E! a e. RR* ( A. b e. x -. a < b /\ A. b e. RR* ( b < a -> E. d e. x b < d ) ) ) )
21 15 20 mpbird 
 |-  ( x C_ RR* -> E! a e. RR* ( A. b e. x b <_ a /\ A. c e. RR* ( A. b e. x b <_ c -> a <_ c ) ) )
22 11 21 sylbi 
 |-  ( x e. ~P RR* -> E! a e. RR* ( A. b e. x b <_ a /\ A. c e. RR* ( A. b e. x b <_ c -> a <_ c ) ) )
23 10 22 mprgbir 
 |-  ~P RR* = { x e. ~P RR* | E! a e. RR* ( A. b e. x b <_ a /\ A. c e. RR* ( A. b e. x b <_ c -> a <_ c ) ) }
24 9 23 eqtr4i 
 |-  dom ( lub ` RR*s ) = ~P RR*
25 eqid 
 |-  ( glb ` RR*s ) = ( glb ` RR*s )
26 biid 
 |-  ( ( A. b e. x a <_ b /\ A. c e. RR* ( A. b e. x c <_ b -> c <_ a ) ) <-> ( A. b e. x a <_ b /\ A. c e. RR* ( A. b e. x c <_ b -> c <_ a ) ) )
27 4 5 25 26 2 glbdm 
 |-  ( RR*s e. Toset -> dom ( glb ` RR*s ) = { x e. ~P RR* | E! a e. RR* ( A. b e. x a <_ b /\ A. c e. RR* ( A. b e. x c <_ b -> c <_ a ) ) } )
28 1 27 ax-mp 
 |-  dom ( glb ` RR*s ) = { x e. ~P RR* | E! a e. RR* ( A. b e. x a <_ b /\ A. c e. RR* ( A. b e. x c <_ b -> c <_ a ) ) }
29 rabid2 
 |-  ( ~P RR* = { x e. ~P RR* | E! a e. RR* ( A. b e. x a <_ b /\ A. c e. RR* ( A. b e. x c <_ b -> c <_ a ) ) } <-> A. x e. ~P RR* E! a e. RR* ( A. b e. x a <_ b /\ A. c e. RR* ( A. b e. x c <_ b -> c <_ a ) ) )
30 cnvso 
 |-  ( < Or RR* <-> `' < Or RR* )
31 12 30 mpbi 
 |-  `' < Or RR*
32 31 a1i 
 |-  ( x C_ RR* -> `' < Or RR* )
33 xrinfmss2 
 |-  ( x C_ RR* -> E. a e. RR* ( A. b e. x -. a `' < b /\ A. b e. RR* ( b `' < a -> E. d e. x b `' < d ) ) )
34 32 33 supeu 
 |-  ( x C_ RR* -> E! a e. RR* ( A. b e. x -. a `' < b /\ A. b e. RR* ( b `' < a -> E. d e. x b `' < d ) ) )
35 4 16 17 18 5 tosglblem 
 |-  ( ( x C_ RR* /\ a e. RR* ) -> ( ( A. b e. x a <_ b /\ A. c e. RR* ( A. b e. x c <_ b -> c <_ a ) ) <-> ( A. b e. x -. a `' < b /\ A. b e. RR* ( b `' < a -> E. d e. x b `' < d ) ) ) )
36 35 reubidva 
 |-  ( x C_ RR* -> ( E! a e. RR* ( A. b e. x a <_ b /\ A. c e. RR* ( A. b e. x c <_ b -> c <_ a ) ) <-> E! a e. RR* ( A. b e. x -. a `' < b /\ A. b e. RR* ( b `' < a -> E. d e. x b `' < d ) ) ) )
37 34 36 mpbird 
 |-  ( x C_ RR* -> E! a e. RR* ( A. b e. x a <_ b /\ A. c e. RR* ( A. b e. x c <_ b -> c <_ a ) ) )
38 11 37 sylbi 
 |-  ( x e. ~P RR* -> E! a e. RR* ( A. b e. x a <_ b /\ A. c e. RR* ( A. b e. x c <_ b -> c <_ a ) ) )
39 29 38 mprgbir 
 |-  ~P RR* = { x e. ~P RR* | E! a e. RR* ( A. b e. x a <_ b /\ A. c e. RR* ( A. b e. x c <_ b -> c <_ a ) ) }
40 28 39 eqtr4i 
 |-  dom ( glb ` RR*s ) = ~P RR*
41 24 40 pm3.2i 
 |-  ( dom ( lub ` RR*s ) = ~P RR* /\ dom ( glb ` RR*s ) = ~P RR* )
42 4 6 25 isclat 
 |-  ( RR*s e. CLat <-> ( RR*s e. Poset /\ ( dom ( lub ` RR*s ) = ~P RR* /\ dom ( glb ` RR*s ) = ~P RR* ) ) )
43 3 41 42 mpbir2an 
 |-  RR*s e. CLat