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 \in ℤ, n \in ℤ ⟼ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}))$
	dya2ioc.2	$⊢ R = (u \in ran I, v \in ran I ⟼ u \times v)$
Assertion	dya2iocuni	$⊢ A \in (J \times_{t} J) \to \exists c \in 𝒫 ran R ⋃ c = A$

Proof

Step	Hyp	Ref	Expression
1		sxbrsiga.0	$⊢ J = topGen (ran (.))$
2		dya2ioc.1	$⊢ I = (x \in ℤ, n \in ℤ ⟼ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}))$
3		dya2ioc.2	$⊢ R = (u \in ran I, v \in ran I ⟼ u \times v)$
4		ssrab2	$⊢ \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} \subseteq ran R$
5	1 2 3	dya2iocrfn	$⊢ R Fn (ran I \times ran I)$
6		zex	$⊢ ℤ \in V$
7	6 6	mpoex	$⊢ (x \in ℤ, n \in ℤ ⟼ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})) \in V$
8	2 7	eqeltri	$⊢ I \in V$
9	8	rnex	$⊢ ran I \in V$
10	9 9	xpex	$⊢ ran I \times ran I \in V$
11		fnex	$⊢ (R Fn (ran I \times ran I) \land ran I \times ran I \in V) \to R \in V$
12	5 10 11	mp2an	$⊢ R \in V$
13	12	rnex	$⊢ ran R \in V$
14	13	elpw2	$⊢ \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} \in 𝒫 ran R \leftrightarrow \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} \subseteq ran R$
15	4 14	mpbir	$⊢ \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} \in 𝒫 ran R$
16	15	a1i	$⊢ A \in (J \times_{t} J) \to \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} \in 𝒫 ran R$
17		rex0	$⊢ \neg \exists z \in \emptyset (z \in b \land b \subseteq A)$
18		rexeq	$⊢ A = \emptyset \to (\exists z \in A (z \in b \land b \subseteq A) \leftrightarrow \exists z \in \emptyset (z \in b \land b \subseteq A))$
19	17 18	mtbiri	$⊢ A = \emptyset \to \neg \exists z \in A (z \in b \land b \subseteq A)$
20	19	ralrimivw	$⊢ A = \emptyset \to \forall b \in ran R \neg \exists z \in A (z \in b \land b \subseteq A)$
21		rabeq0	$⊢ \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} = \emptyset \leftrightarrow \forall b \in ran R \neg \exists z \in A (z \in b \land b \subseteq A)$
22	20 21	sylibr	$⊢ A = \emptyset \to \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} = \emptyset$
23	22	unieqd	$⊢ A = \emptyset \to ⋃ \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} = ⋃ \emptyset$
24		uni0	$⊢ ⋃ \emptyset = \emptyset$
25	23 24	eqtrdi	$⊢ A = \emptyset \to ⋃ \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} = \emptyset$
26		0ss	$⊢ \emptyset \subseteq A$
27	25 26	eqsstrdi	$⊢ A = \emptyset \to ⋃ \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} \subseteq A$
28		elequ2	$⊢ b = p \to (z \in b \leftrightarrow z \in p)$
29		sseq1	$⊢ b = p \to (b \subseteq A \leftrightarrow p \subseteq A)$
30	28 29	anbi12d	$⊢ b = p \to ((z \in b \land b \subseteq A) \leftrightarrow (z \in p \land p \subseteq A))$
31	30	rexbidv	$⊢ b = p \to (\exists z \in A (z \in b \land b \subseteq A) \leftrightarrow \exists z \in A (z \in p \land p \subseteq A))$
32	31	elrab	$⊢ p \in \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} \leftrightarrow (p \in ran R \land \exists z \in A (z \in p \land p \subseteq A))$
33		simpr	$⊢ (z \in p \land p \subseteq A) \to p \subseteq A$
34	33	reximi	$⊢ \exists z \in A (z \in p \land p \subseteq A) \to \exists z \in A p \subseteq A$
35		r19.9rzv	$⊢ A \neq \emptyset \to (p \subseteq A \leftrightarrow \exists z \in A p \subseteq A)$
36	34 35	imbitrrid	$⊢ A \neq \emptyset \to (\exists z \in A (z \in p \land p \subseteq A) \to p \subseteq A)$
37	36	adantld	$⊢ A \neq \emptyset \to ((p \in ran R \land \exists z \in A (z \in p \land p \subseteq A)) \to p \subseteq A)$
38	32 37	biimtrid	$⊢ A \neq \emptyset \to (p \in \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} \to p \subseteq A)$
39	38	ralrimiv	$⊢ A \neq \emptyset \to \forall p \in \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} p \subseteq A$
40		unissb	$⊢ ⋃ \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} \subseteq A \leftrightarrow \forall p \in \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} p \subseteq A$
41	39 40	sylibr	$⊢ A \neq \emptyset \to ⋃ \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} \subseteq A$
42	27 41	pm2.61ine	$⊢ ⋃ \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} \subseteq A$
43	42	a1i	$⊢ A \in (J \times_{t} J) \to ⋃ \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} \subseteq A$
44	1 2 3	dya2iocnei	$⊢ (A \in (J \times_{t} J) \land m \in A) \to \exists p \in ran R (m \in p \land p \subseteq A)$
45		simpl	$⊢ (p \in ran R \land (m \in p \land p \subseteq A)) \to p \in ran R$
46		ssel2	$⊢ (p \subseteq A \land m \in p) \to m \in A$
47	46	ancoms	$⊢ (m \in p \land p \subseteq A) \to m \in A$
48	47	adantl	$⊢ (p \in ran R \land (m \in p \land p \subseteq A)) \to m \in A$
49		simpr	$⊢ (p \in ran R \land (m \in p \land p \subseteq A)) \to (m \in p \land p \subseteq A)$
50		elequ1	$⊢ z = m \to (z \in p \leftrightarrow m \in p)$
51	50	anbi1d	$⊢ z = m \to ((z \in p \land p \subseteq A) \leftrightarrow (m \in p \land p \subseteq A))$
52	51	rspcev	$⊢ (m \in A \land (m \in p \land p \subseteq A)) \to \exists z \in A (z \in p \land p \subseteq A)$
53	48 49 52	syl2anc	$⊢ (p \in ran R \land (m \in p \land p \subseteq A)) \to \exists z \in A (z \in p \land p \subseteq A)$
54	45 53	jca	$⊢ (p \in ran R \land (m \in p \land p \subseteq A)) \to (p \in ran R \land \exists z \in A (z \in p \land p \subseteq A))$
55	54 32	sylibr	$⊢ (p \in ran R \land (m \in p \land p \subseteq A)) \to p \in \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\}$
56		simprl	$⊢ (p \in ran R \land (m \in p \land p \subseteq A)) \to m \in p$
57	55 56	jca	$⊢ (p \in ran R \land (m \in p \land p \subseteq A)) \to (p \in \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} \land m \in p)$
58	57	reximi2	$⊢ \exists p \in ran R (m \in p \land p \subseteq A) \to \exists p \in \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} m \in p$
59	44 58	syl	$⊢ (A \in (J \times_{t} J) \land m \in A) \to \exists p \in \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} m \in p$
60		eluni2	$⊢ m \in ⋃ \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} \leftrightarrow \exists p \in \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} m \in p$
61	59 60	sylibr	$⊢ (A \in (J \times_{t} J) \land m \in A) \to m \in ⋃ \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\}$
62	43 61	eqelssd	$⊢ A \in (J \times_{t} J) \to ⋃ \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} = A$
63		unieq	$⊢ c = \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} \to ⋃ c = ⋃ \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\}$
64	63	eqeq1d	$⊢ c = \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} \to (⋃ c = A \leftrightarrow ⋃ \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} = A)$
65	64	rspcev	$⊢ (\{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} \in 𝒫 ran R \land ⋃ \{b \in ran R \| \exists z \in A (z \in b \land b \subseteq A)\} = A) \to \exists c \in 𝒫 ran R ⋃ c = A$
66	16 62 65	syl2anc	$⊢ A \in (J \times_{t} J) \to \exists c \in 𝒫 ran R ⋃ c = A$

Metamath Proof Explorer

Theorem dya2iocuni

Proof