Metamath Proof Explorer

Theorem sxbrsigalem0

Description: The closed half-spaces of ( RR X. RR ) cover ( RR X. RR ) . (Contributed by Thierry Arnoux, 11-Oct-2017)

Ref Expression
Assertion sxbrsigalem0 
|- U. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) = ( RR X. RR )

Proof

Step Hyp Ref Expression
1 unissb 
 |-  ( U. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) C_ ( RR X. RR ) <-> A. z e. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) z C_ ( RR X. RR ) )
2 elun 
 |-  ( z e. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) <-> ( z e. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) \/ z e. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) )
3 eqid 
 |-  ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) = ( e e. RR |-> ( ( e [,) +oo ) X. RR ) )
4 3 rnmptss 
 |-  ( A. e e. RR ( ( e [,) +oo ) X. RR ) e. ~P ( RR X. RR ) -> ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) C_ ~P ( RR X. RR ) )
5 pnfxr 
 |-  +oo e. RR*
6 icossre 
 |-  ( ( e e. RR /\ +oo e. RR* ) -> ( e [,) +oo ) C_ RR )
7 5 6 mpan2 
 |-  ( e e. RR -> ( e [,) +oo ) C_ RR )
8 xpss1 
 |-  ( ( e [,) +oo ) C_ RR -> ( ( e [,) +oo ) X. RR ) C_ ( RR X. RR ) )
9 7 8 syl 
 |-  ( e e. RR -> ( ( e [,) +oo ) X. RR ) C_ ( RR X. RR ) )
10 ovex 
 |-  ( e [,) +oo ) e. _V
11 reex 
 |-  RR e. _V
12 10 11 xpex 
 |-  ( ( e [,) +oo ) X. RR ) e. _V
13 12 elpw 
 |-  ( ( ( e [,) +oo ) X. RR ) e. ~P ( RR X. RR ) <-> ( ( e [,) +oo ) X. RR ) C_ ( RR X. RR ) )
14 9 13 sylibr 
 |-  ( e e. RR -> ( ( e [,) +oo ) X. RR ) e. ~P ( RR X. RR ) )
15 4 14 mprg 
 |-  ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) C_ ~P ( RR X. RR )
16 15 sseli 
 |-  ( z e. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) -> z e. ~P ( RR X. RR ) )
17 16 elpwid 
 |-  ( z e. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) -> z C_ ( RR X. RR ) )
18 eqid 
 |-  ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) = ( f e. RR |-> ( RR X. ( f [,) +oo ) ) )
19 18 rnmptss 
 |-  ( A. f e. RR ( RR X. ( f [,) +oo ) ) e. ~P ( RR X. RR ) -> ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) C_ ~P ( RR X. RR ) )
20 icossre 
 |-  ( ( f e. RR /\ +oo e. RR* ) -> ( f [,) +oo ) C_ RR )
21 5 20 mpan2 
 |-  ( f e. RR -> ( f [,) +oo ) C_ RR )
22 xpss2 
 |-  ( ( f [,) +oo ) C_ RR -> ( RR X. ( f [,) +oo ) ) C_ ( RR X. RR ) )
23 21 22 syl 
 |-  ( f e. RR -> ( RR X. ( f [,) +oo ) ) C_ ( RR X. RR ) )
24 ovex 
 |-  ( f [,) +oo ) e. _V
25 11 24 xpex 
 |-  ( RR X. ( f [,) +oo ) ) e. _V
26 25 elpw 
 |-  ( ( RR X. ( f [,) +oo ) ) e. ~P ( RR X. RR ) <-> ( RR X. ( f [,) +oo ) ) C_ ( RR X. RR ) )
27 23 26 sylibr 
 |-  ( f e. RR -> ( RR X. ( f [,) +oo ) ) e. ~P ( RR X. RR ) )
28 19 27 mprg 
 |-  ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) C_ ~P ( RR X. RR )
29 28 sseli 
 |-  ( z e. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) -> z e. ~P ( RR X. RR ) )
30 29 elpwid 
 |-  ( z e. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) -> z C_ ( RR X. RR ) )
31 17 30 jaoi 
 |-  ( ( z e. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) \/ z e. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) -> z C_ ( RR X. RR ) )
32 2 31 sylbi 
 |-  ( z e. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) -> z C_ ( RR X. RR ) )
33 1 32 mprgbir 
 |-  U. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) C_ ( RR X. RR )
34 funmpt 
 |-  Fun ( e e. RR |-> ( ( e [,) +oo ) X. RR ) )
35 rexr 
 |-  ( ( 1st ` z ) e. RR -> ( 1st ` z ) e. RR* )
36 5 a1i 
 |-  ( ( 1st ` z ) e. RR -> +oo e. RR* )
37 ltpnf 
 |-  ( ( 1st ` z ) e. RR -> ( 1st ` z ) < +oo )
38 lbico1 
 |-  ( ( ( 1st ` z ) e. RR* /\ +oo e. RR* /\ ( 1st ` z ) < +oo ) -> ( 1st ` z ) e. ( ( 1st ` z ) [,) +oo ) )
39 35 36 37 38 syl3anc 
 |-  ( ( 1st ` z ) e. RR -> ( 1st ` z ) e. ( ( 1st ` z ) [,) +oo ) )
40 39 anim1i 
 |-  ( ( ( 1st ` z ) e. RR /\ ( 2nd ` z ) e. RR ) -> ( ( 1st ` z ) e. ( ( 1st ` z ) [,) +oo ) /\ ( 2nd ` z ) e. RR ) )
41 40 anim2i 
 |-  ( ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. RR /\ ( 2nd ` z ) e. RR ) ) -> ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. ( ( 1st ` z ) [,) +oo ) /\ ( 2nd ` z ) e. RR ) ) )
42 elxp7 
 |-  ( z e. ( RR X. RR ) <-> ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. RR /\ ( 2nd ` z ) e. RR ) ) )
43 elxp7 
 |-  ( z e. ( ( ( 1st ` z ) [,) +oo ) X. RR ) <-> ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. ( ( 1st ` z ) [,) +oo ) /\ ( 2nd ` z ) e. RR ) ) )
44 41 42 43 3imtr4i 
 |-  ( z e. ( RR X. RR ) -> z e. ( ( ( 1st ` z ) [,) +oo ) X. RR ) )
45 xp1st 
 |-  ( z e. ( RR X. RR ) -> ( 1st ` z ) e. RR )
46 oveq1 
 |-  ( e = ( 1st ` z ) -> ( e [,) +oo ) = ( ( 1st ` z ) [,) +oo ) )
47 46 xpeq1d 
 |-  ( e = ( 1st ` z ) -> ( ( e [,) +oo ) X. RR ) = ( ( ( 1st ` z ) [,) +oo ) X. RR ) )
48 ovex 
 |-  ( ( 1st ` z ) [,) +oo ) e. _V
49 48 11 xpex 
 |-  ( ( ( 1st ` z ) [,) +oo ) X. RR ) e. _V
50 47 3 49 fvmpt 
 |-  ( ( 1st ` z ) e. RR -> ( ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) ` ( 1st ` z ) ) = ( ( ( 1st ` z ) [,) +oo ) X. RR ) )
51 45 50 syl 
 |-  ( z e. ( RR X. RR ) -> ( ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) ` ( 1st ` z ) ) = ( ( ( 1st ` z ) [,) +oo ) X. RR ) )
52 44 51 eleqtrrd 
 |-  ( z e. ( RR X. RR ) -> z e. ( ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) ` ( 1st ` z ) ) )
53 elunirn2 
 |-  ( ( Fun ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) /\ z e. ( ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) ` ( 1st ` z ) ) ) -> z e. U. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) )
54 34 52 53 sylancr 
 |-  ( z e. ( RR X. RR ) -> z e. U. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) )
55 54 ssriv 
 |-  ( RR X. RR ) C_ U. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) )
56 ssun3 
 |-  ( ( RR X. RR ) C_ U. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) -> ( RR X. RR ) C_ ( U. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. U. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) )
57 55 56 ax-mp 
 |-  ( RR X. RR ) C_ ( U. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. U. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) )
58 uniun 
 |-  U. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) = ( U. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. U. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) )
59 57 58 sseqtrri 
 |-  ( RR X. RR ) C_ U. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) )
60 33 59 eqssi 
 |-  U. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) = ( RR X. RR )