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 rexr 
 |-  ( ( 1st ` z ) e. RR -> ( 1st ` z ) e. RR* )
35 5 a1i 
 |-  ( ( 1st ` z ) e. RR -> +oo e. RR* )
36 ltpnf 
 |-  ( ( 1st ` z ) e. RR -> ( 1st ` z ) < +oo )
37 lbico1 
 |-  ( ( ( 1st ` z ) e. RR* /\ +oo e. RR* /\ ( 1st ` z ) < +oo ) -> ( 1st ` z ) e. ( ( 1st ` z ) [,) +oo ) )
38 34 35 36 37 syl3anc 
 |-  ( ( 1st ` z ) e. RR -> ( 1st ` z ) e. ( ( 1st ` z ) [,) +oo ) )
39 38 anim1i 
 |-  ( ( ( 1st ` z ) e. RR /\ ( 2nd ` z ) e. RR ) -> ( ( 1st ` z ) e. ( ( 1st ` z ) [,) +oo ) /\ ( 2nd ` z ) e. RR ) )
40 39 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 ) ) )
41 elxp7 
 |-  ( z e. ( RR X. RR ) <-> ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. RR /\ ( 2nd ` z ) e. RR ) ) )
42 elxp7 
 |-  ( z e. ( ( ( 1st ` z ) [,) +oo ) X. RR ) <-> ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. ( ( 1st ` z ) [,) +oo ) /\ ( 2nd ` z ) e. RR ) ) )
43 40 41 42 3imtr4i 
 |-  ( z e. ( RR X. RR ) -> z e. ( ( ( 1st ` z ) [,) +oo ) X. RR ) )
44 xp1st 
 |-  ( z e. ( RR X. RR ) -> ( 1st ` z ) e. RR )
45 oveq1 
 |-  ( e = ( 1st ` z ) -> ( e [,) +oo ) = ( ( 1st ` z ) [,) +oo ) )
46 45 xpeq1d 
 |-  ( e = ( 1st ` z ) -> ( ( e [,) +oo ) X. RR ) = ( ( ( 1st ` z ) [,) +oo ) X. RR ) )
47 ovex 
 |-  ( ( 1st ` z ) [,) +oo ) e. _V
48 47 11 xpex 
 |-  ( ( ( 1st ` z ) [,) +oo ) X. RR ) e. _V
49 46 3 48 fvmpt 
 |-  ( ( 1st ` z ) e. RR -> ( ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) ` ( 1st ` z ) ) = ( ( ( 1st ` z ) [,) +oo ) X. RR ) )
50 44 49 syl 
 |-  ( z e. ( RR X. RR ) -> ( ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) ` ( 1st ` z ) ) = ( ( ( 1st ` z ) [,) +oo ) X. RR ) )
51 43 50 eleqtrrd 
 |-  ( z e. ( RR X. RR ) -> z e. ( ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) ` ( 1st ` z ) ) )
52 elfvunirn 
 |-  ( z e. ( ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) ` ( 1st ` z ) ) -> z e. U. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) )
53 51 52 syl 
 |-  ( z e. ( RR X. RR ) -> z e. U. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) )
54 53 ssriv 
 |-  ( RR X. RR ) C_ U. ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) )
55 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 ) ) ) ) )
56 54 55 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 ) ) ) )
57 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 ) ) ) )
58 56 57 sseqtrri 
 |-  ( RR X. RR ) C_ U. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) )
59 33 58 eqssi 
 |-  U. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) = ( RR X. RR )