Metamath Proof Explorer

Theorem dya2iocuni

Description: Every open set of ( RR X. RR ) is a union of closed-below open-above dyadic rational rectangular subsets of ( RR X. RR ) . This union must be a countable union by dya2iocct . (Contributed by Thierry Arnoux, 18-Sep-2017)

Ref Expression
Hypotheses sxbrsiga.0 
|- J = ( topGen ` ran (,) )
dya2ioc.1 
|- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
dya2ioc.2 
|- R = ( u e. ran I , v e. ran I |-> ( u X. v ) )
Assertion dya2iocuni 
|- ( A e. ( J tX J ) -> E. c e. ~P ran R U. c = A )

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 
 |-  J = ( topGen ` ran (,) )
2 dya2ioc.1 
 |-  I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
3 dya2ioc.2 
 |-  R = ( u e. ran I , v e. ran I |-> ( u X. v ) )
4 ssrab2 
 |-  { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } C_ ran R
5 1 2 3 dya2iocrfn 
 |-  R Fn ( ran I X. ran I )
6 zex 
 |-  ZZ e. _V
7 6 6 mpoex 
 |-  ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) e. _V
8 2 7 eqeltri 
 |-  I e. _V
9 8 rnex 
 |-  ran I e. _V
10 9 9 xpex 
 |-  ( ran I X. ran I ) e. _V
11 fnex 
 |-  ( ( R Fn ( ran I X. ran I ) /\ ( ran I X. ran I ) e. _V ) -> R e. _V )
12 5 10 11 mp2an 
 |-  R e. _V
13 12 rnex 
 |-  ran R e. _V
14 13 elpw2 
 |-  ( { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } e. ~P ran R <-> { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } C_ ran R )
15 4 14 mpbir 
 |-  { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } e. ~P ran R
16 15 a1i 
 |-  ( A e. ( J tX J ) -> { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } e. ~P ran R )
17 rex0 
 |-  -. E. z e. (/) ( z e. b /\ b C_ A )
18 rexeq 
 |-  ( A = (/) -> ( E. z e. A ( z e. b /\ b C_ A ) <-> E. z e. (/) ( z e. b /\ b C_ A ) ) )
19 17 18 mtbiri 
 |-  ( A = (/) -> -. E. z e. A ( z e. b /\ b C_ A ) )
20 19 ralrimivw 
 |-  ( A = (/) -> A. b e. ran R -. E. z e. A ( z e. b /\ b C_ A ) )
21 rabeq0 
 |-  ( { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } = (/) <-> A. b e. ran R -. E. z e. A ( z e. b /\ b C_ A ) )
22 20 21 sylibr 
 |-  ( A = (/) -> { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } = (/) )
23 22 unieqd 
 |-  ( A = (/) -> U. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } = U. (/) )
24 uni0 
 |-  U. (/) = (/)
25 23 24 eqtrdi 
 |-  ( A = (/) -> U. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } = (/) )
26 0ss 
 |-  (/) C_ A
27 25 26 eqsstrdi 
 |-  ( A = (/) -> U. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } C_ A )
28 elequ2 
 |-  ( b = p -> ( z e. b <-> z e. p ) )
29 sseq1 
 |-  ( b = p -> ( b C_ A <-> p C_ A ) )
30 28 29 anbi12d 
 |-  ( b = p -> ( ( z e. b /\ b C_ A ) <-> ( z e. p /\ p C_ A ) ) )
31 30 rexbidv 
 |-  ( b = p -> ( E. z e. A ( z e. b /\ b C_ A ) <-> E. z e. A ( z e. p /\ p C_ A ) ) )
32 31 elrab 
 |-  ( p e. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } <-> ( p e. ran R /\ E. z e. A ( z e. p /\ p C_ A ) ) )
33 simpr 
 |-  ( ( z e. p /\ p C_ A ) -> p C_ A )
34 33 reximi 
 |-  ( E. z e. A ( z e. p /\ p C_ A ) -> E. z e. A p C_ A )
35 r19.9rzv 
 |-  ( A =/= (/) -> ( p C_ A <-> E. z e. A p C_ A ) )
36 34 35 syl5ibr 
 |-  ( A =/= (/) -> ( E. z e. A ( z e. p /\ p C_ A ) -> p C_ A ) )
37 36 adantld 
 |-  ( A =/= (/) -> ( ( p e. ran R /\ E. z e. A ( z e. p /\ p C_ A ) ) -> p C_ A ) )
38 32 37 syl5bi 
 |-  ( A =/= (/) -> ( p e. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } -> p C_ A ) )
39 38 ralrimiv 
 |-  ( A =/= (/) -> A. p e. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } p C_ A )
40 unissb 
 |-  ( U. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } C_ A <-> A. p e. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } p C_ A )
41 39 40 sylibr 
 |-  ( A =/= (/) -> U. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } C_ A )
42 27 41 pm2.61ine 
 |-  U. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } C_ A
43 42 a1i 
 |-  ( A e. ( J tX J ) -> U. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } C_ A )
44 1 2 3 dya2iocnei 
 |-  ( ( A e. ( J tX J ) /\ m e. A ) -> E. p e. ran R ( m e. p /\ p C_ A ) )
45 simpl 
 |-  ( ( p e. ran R /\ ( m e. p /\ p C_ A ) ) -> p e. ran R )
46 ssel2 
 |-  ( ( p C_ A /\ m e. p ) -> m e. A )
47 46 ancoms 
 |-  ( ( m e. p /\ p C_ A ) -> m e. A )
48 47 adantl 
 |-  ( ( p e. ran R /\ ( m e. p /\ p C_ A ) ) -> m e. A )
49 simpr 
 |-  ( ( p e. ran R /\ ( m e. p /\ p C_ A ) ) -> ( m e. p /\ p C_ A ) )
50 elequ1 
 |-  ( z = m -> ( z e. p <-> m e. p ) )
51 50 anbi1d 
 |-  ( z = m -> ( ( z e. p /\ p C_ A ) <-> ( m e. p /\ p C_ A ) ) )
52 51 rspcev 
 |-  ( ( m e. A /\ ( m e. p /\ p C_ A ) ) -> E. z e. A ( z e. p /\ p C_ A ) )
53 48 49 52 syl2anc 
 |-  ( ( p e. ran R /\ ( m e. p /\ p C_ A ) ) -> E. z e. A ( z e. p /\ p C_ A ) )
54 45 53 jca 
 |-  ( ( p e. ran R /\ ( m e. p /\ p C_ A ) ) -> ( p e. ran R /\ E. z e. A ( z e. p /\ p C_ A ) ) )
55 54 32 sylibr 
 |-  ( ( p e. ran R /\ ( m e. p /\ p C_ A ) ) -> p e. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } )
56 simprl 
 |-  ( ( p e. ran R /\ ( m e. p /\ p C_ A ) ) -> m e. p )
57 55 56 jca 
 |-  ( ( p e. ran R /\ ( m e. p /\ p C_ A ) ) -> ( p e. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } /\ m e. p ) )
58 57 reximi2 
 |-  ( E. p e. ran R ( m e. p /\ p C_ A ) -> E. p e. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } m e. p )
59 44 58 syl 
 |-  ( ( A e. ( J tX J ) /\ m e. A ) -> E. p e. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } m e. p )
60 eluni2 
 |-  ( m e. U. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } <-> E. p e. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } m e. p )
61 59 60 sylibr 
 |-  ( ( A e. ( J tX J ) /\ m e. A ) -> m e. U. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } )
62 43 61 eqelssd 
 |-  ( A e. ( J tX J ) -> U. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } = A )
63 unieq 
 |-  ( c = { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } -> U. c = U. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } )
64 63 eqeq1d 
 |-  ( c = { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } -> ( U. c = A <-> U. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } = A ) )
65 64 rspcev 
 |-  ( ( { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } e. ~P ran R /\ U. { b e. ran R | E. z e. A ( z e. b /\ b C_ A ) } = A ) -> E. c e. ~P ran R U. c = A )
66 16 62 65 syl2anc 
 |-  ( A e. ( J tX J ) -> E. c e. ~P ran R U. c = A )