dya2iocnrect

Description: For any point of an open rectangle in ( RR X. RR ) , there is a closed-below open-above dyadic rational square which contains that point and is included in the rectangle. (Contributed by Thierry Arnoux, 12-Oct-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)$
	dya2iocnrect.1	$⊢ B = ran (e \in ran (.), f \in ran (.) ⟼ e \times f)$
Assertion	dya2iocnrect	$⊢ (X \in ℝ^{2} \land A \in B \land X \in A) \to \exists b \in ran R (X \in b \land b \subseteq 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		dya2iocnrect.1	$⊢ B = ran (e \in ran (.), f \in ran (.) ⟼ e \times f)$
5	4	eleq2i	$⊢ A \in B \leftrightarrow A \in ran (e \in ran (.), f \in ran (.) ⟼ e \times f)$
6		eqid	$⊢ (e \in ran (.), f \in ran (.) ⟼ e \times f) = (e \in ran (.), f \in ran (.) ⟼ e \times f)$
7		vex	$⊢ e \in V$
8		vex	$⊢ f \in V$
9	7 8	xpex	$⊢ e \times f \in V$
10	6 9	elrnmpo	$⊢ A \in ran (e \in ran (.), f \in ran (.) ⟼ e \times f) \leftrightarrow \exists e \in ran (.) \exists f \in ran (.) A = e \times f$
11	5 10	sylbb	$⊢ A \in B \to \exists e \in ran (.) \exists f \in ran (.) A = e \times f$
12	11	3ad2ant2	$⊢ (X \in ℝ^{2} \land A \in B \land X \in A) \to \exists e \in ran (.) \exists f \in ran (.) A = e \times f$
13		simp1	$⊢ (X \in ℝ^{2} \land A \in B \land X \in A) \to X \in ℝ^{2}$
14		simp3	$⊢ (X \in ℝ^{2} \land A \in B \land X \in A) \to X \in A$
15	12 13 14	jca32	$⊢ (X \in ℝ^{2} \land A \in B \land X \in A) \to (\exists e \in ran (.) \exists f \in ran (.) A = e \times f \land (X \in ℝ^{2} \land X \in A))$
16		r19.41vv	$⊢ \exists e \in ran (.) \exists f \in ran (.) (A = e \times f \land (X \in ℝ^{2} \land X \in A)) \leftrightarrow (\exists e \in ran (.) \exists f \in ran (.) A = e \times f \land (X \in ℝ^{2} \land X \in A))$
17	16	biimpri	$⊢ (\exists e \in ran (.) \exists f \in ran (.) A = e \times f \land (X \in ℝ^{2} \land X \in A)) \to \exists e \in ran (.) \exists f \in ran (.) (A = e \times f \land (X \in ℝ^{2} \land X \in A))$
18		simprl	$⊢ (A = e \times f \land (X \in ℝ^{2} \land X \in A)) \to X \in ℝ^{2}$
19		simpl	$⊢ (A = e \times f \land (X \in ℝ^{2} \land X \in A)) \to A = e \times f$
20		simprr	$⊢ (A = e \times f \land (X \in ℝ^{2} \land X \in A)) \to X \in A$
21	20 19	eleqtrd	$⊢ (A = e \times f \land (X \in ℝ^{2} \land X \in A)) \to X \in (e \times f)$
22	18 19 21	3jca	$⊢ (A = e \times f \land (X \in ℝ^{2} \land X \in A)) \to (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f))$
23		simpr	$⊢ ((e \in ran (.) \land f \in ran (.)) \land (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f))) \to (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f))$
24		xp1st	$⊢ X \in ℝ^{2} \to 1^{st} (X) \in ℝ$
25	24	3ad2ant1	$⊢ (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \to 1^{st} (X) \in ℝ$
26	25	adantl	$⊢ ((e \in ran (.) \land f \in ran (.)) \land (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f))) \to 1^{st} (X) \in ℝ$
27		simpll	$⊢ ((e \in ran (.) \land f \in ran (.)) \land (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f))) \to e \in ran (.)$
28		xp1st	$⊢ X \in (e \times f) \to 1^{st} (X) \in e$
29	28	3ad2ant3	$⊢ (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \to 1^{st} (X) \in e$
30	29	adantl	$⊢ ((e \in ran (.) \land f \in ran (.)) \land (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f))) \to 1^{st} (X) \in e$
31	1 2	dya2icoseg2	$⊢ (1^{st} (X) \in ℝ \land e \in ran (.) \land 1^{st} (X) \in e) \to \exists s \in ran I (1^{st} (X) \in s \land s \subseteq e)$
32	26 27 30 31	syl3anc	$⊢ ((e \in ran (.) \land f \in ran (.)) \land (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f))) \to \exists s \in ran I (1^{st} (X) \in s \land s \subseteq e)$
33		xp2nd	$⊢ X \in ℝ^{2} \to 2^{nd} (X) \in ℝ$
34	33	3ad2ant1	$⊢ (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \to 2^{nd} (X) \in ℝ$
35	34	adantl	$⊢ ((e \in ran (.) \land f \in ran (.)) \land (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f))) \to 2^{nd} (X) \in ℝ$
36		simplr	$⊢ ((e \in ran (.) \land f \in ran (.)) \land (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f))) \to f \in ran (.)$
37		xp2nd	$⊢ X \in (e \times f) \to 2^{nd} (X) \in f$
38	37	3ad2ant3	$⊢ (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \to 2^{nd} (X) \in f$
39	38	adantl	$⊢ ((e \in ran (.) \land f \in ran (.)) \land (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f))) \to 2^{nd} (X) \in f$
40	1 2	dya2icoseg2	$⊢ (2^{nd} (X) \in ℝ \land f \in ran (.) \land 2^{nd} (X) \in f) \to \exists t \in ran I (2^{nd} (X) \in t \land t \subseteq f)$
41	35 36 39 40	syl3anc	$⊢ ((e \in ran (.) \land f \in ran (.)) \land (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f))) \to \exists t \in ran I (2^{nd} (X) \in t \land t \subseteq f)$
42		reeanv	$⊢ \exists s \in ran I \exists t \in ran I ((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f)) \leftrightarrow (\exists s \in ran I (1^{st} (X) \in s \land s \subseteq e) \land \exists t \in ran I (2^{nd} (X) \in t \land t \subseteq f))$
43	32 41 42	sylanbrc	$⊢ ((e \in ran (.) \land f \in ran (.)) \land (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f))) \to \exists s \in ran I \exists t \in ran I ((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f))$
44		eqid	$⊢ s \times t = s \times t$
45		xpeq1	$⊢ u = s \to u \times v = s \times v$
46	45	eqeq2d	$⊢ u = s \to (s \times t = u \times v \leftrightarrow s \times t = s \times v)$
47		xpeq2	$⊢ v = t \to s \times v = s \times t$
48	47	eqeq2d	$⊢ v = t \to (s \times t = s \times v \leftrightarrow s \times t = s \times t)$
49	46 48	rspc2ev	$⊢ (s \in ran I \land t \in ran I \land s \times t = s \times t) \to \exists u \in ran I \exists v \in ran I s \times t = u \times v$
50	44 49	mp3an3	$⊢ (s \in ran I \land t \in ran I) \to \exists u \in ran I \exists v \in ran I s \times t = u \times v$
51		vex	$⊢ u \in V$
52		vex	$⊢ v \in V$
53	51 52	xpex	$⊢ u \times v \in V$
54	3 53	elrnmpo	$⊢ s \times t \in ran R \leftrightarrow \exists u \in ran I \exists v \in ran I s \times t = u \times v$
55	50 54	sylibr	$⊢ (s \in ran I \land t \in ran I) \to s \times t \in ran R$
56	55	ad2antrl	$⊢ ((X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \land ((s \in ran I \land t \in ran I) \land ((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f)))) \to s \times t \in ran R$
57		xpss	$⊢ ℝ^{2} \subseteq V \times V$
58		simpl1	$⊢ ((X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \land ((s \in ran I \land t \in ran I) \land ((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f)))) \to X \in ℝ^{2}$
59	57 58	sseldi	$⊢ ((X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \land ((s \in ran I \land t \in ran I) \land ((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f)))) \to X \in (V \times V)$
60		simprrl	$⊢ ((X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \land ((s \in ran I \land t \in ran I) \land ((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f)))) \to (1^{st} (X) \in s \land s \subseteq e)$
61	60	simpld	$⊢ ((X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \land ((s \in ran I \land t \in ran I) \land ((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f)))) \to 1^{st} (X) \in s$
62		simprrr	$⊢ ((X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \land ((s \in ran I \land t \in ran I) \land ((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f)))) \to (2^{nd} (X) \in t \land t \subseteq f)$
63	62	simpld	$⊢ ((X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \land ((s \in ran I \land t \in ran I) \land ((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f)))) \to 2^{nd} (X) \in t$
64		elxp7	$⊢ X \in (s \times t) \leftrightarrow (X \in (V \times V) \land (1^{st} (X) \in s \land 2^{nd} (X) \in t))$
65	64	biimpri	$⊢ (X \in (V \times V) \land (1^{st} (X) \in s \land 2^{nd} (X) \in t)) \to X \in (s \times t)$
66	59 61 63 65	syl12anc	$⊢ ((X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \land ((s \in ran I \land t \in ran I) \land ((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f)))) \to X \in (s \times t)$
67	60	simprd	$⊢ ((X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \land ((s \in ran I \land t \in ran I) \land ((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f)))) \to s \subseteq e$
68	62	simprd	$⊢ ((X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \land ((s \in ran I \land t \in ran I) \land ((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f)))) \to t \subseteq f$
69		xpss12	$⊢ (s \subseteq e \land t \subseteq f) \to s \times t \subseteq e \times f$
70	67 68 69	syl2anc	$⊢ ((X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \land ((s \in ran I \land t \in ran I) \land ((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f)))) \to s \times t \subseteq e \times f$
71		simpl2	$⊢ ((X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \land ((s \in ran I \land t \in ran I) \land ((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f)))) \to A = e \times f$
72	70 71	sseqtrrd	$⊢ ((X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \land ((s \in ran I \land t \in ran I) \land ((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f)))) \to s \times t \subseteq A$
73		eleq2	$⊢ b = s \times t \to (X \in b \leftrightarrow X \in (s \times t))$
74		sseq1	$⊢ b = s \times t \to (b \subseteq A \leftrightarrow s \times t \subseteq A)$
75	73 74	anbi12d	$⊢ b = s \times t \to ((X \in b \land b \subseteq A) \leftrightarrow (X \in (s \times t) \land s \times t \subseteq A))$
76	75	rspcev	$⊢ (s \times t \in ran R \land (X \in (s \times t) \land s \times t \subseteq A)) \to \exists b \in ran R (X \in b \land b \subseteq A)$
77	56 66 72 76	syl12anc	$⊢ ((X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \land ((s \in ran I \land t \in ran I) \land ((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f)))) \to \exists b \in ran R (X \in b \land b \subseteq A)$
78	77	exp32	$⊢ (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \to ((s \in ran I \land t \in ran I) \to (((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f)) \to \exists b \in ran R (X \in b \land b \subseteq A)))$
79	78	rexlimdvv	$⊢ (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f)) \to (\exists s \in ran I \exists t \in ran I ((1^{st} (X) \in s \land s \subseteq e) \land (2^{nd} (X) \in t \land t \subseteq f)) \to \exists b \in ran R (X \in b \land b \subseteq A))$
80	23 43 79	sylc	$⊢ ((e \in ran (.) \land f \in ran (.)) \land (X \in ℝ^{2} \land A = e \times f \land X \in (e \times f))) \to \exists b \in ran R (X \in b \land b \subseteq A)$
81	22 80	sylan2	$⊢ ((e \in ran (.) \land f \in ran (.)) \land (A = e \times f \land (X \in ℝ^{2} \land X \in A))) \to \exists b \in ran R (X \in b \land b \subseteq A)$
82	81	ex	$⊢ (e \in ran (.) \land f \in ran (.)) \to ((A = e \times f \land (X \in ℝ^{2} \land X \in A)) \to \exists b \in ran R (X \in b \land b \subseteq A))$
83	82	rexlimivv	$⊢ \exists e \in ran (.) \exists f \in ran (.) (A = e \times f \land (X \in ℝ^{2} \land X \in A)) \to \exists b \in ran R (X \in b \land b \subseteq A)$
84	15 17 83	3syl	$⊢ (X \in ℝ^{2} \land A \in B \land X \in A) \to \exists b \in ran R (X \in b \land b \subseteq A)$

Metamath Proof Explorer

Theorem dya2iocnrect

Proof