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	imbitrrid	|- ( 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	biimtrid	|- ( 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 )