Metamath Proof Explorer

Theorem isbasisrelowllem1

Description: Lemma for isbasisrelowl . (Contributed by ML, 27-Jul-2020)

Ref Expression
Hypothesis isbasisrelowl.1 ⊢ I = . ℝ 2
Assertion isbasisrelowllem1 ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → x ∩ y ∈ I

Proof

Step Hyp Ref Expression
1 isbasisrelowl.1 ⊢ I = . ℝ 2
2 simplr1 ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → c ∈ ℝ
3 simpll2 ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → b ∈ ℝ
4 nfv ⊢ Ⅎ z a ∈ ℝ
5 nfv ⊢ Ⅎ z b ∈ ℝ
6 nfrab1 ⊢ Ⅎ _ z z ∈ ℝ | a ≤ z ∧ z < b
7 6 nfeq2 ⊢ Ⅎ z x = z ∈ ℝ | a ≤ z ∧ z < b
8 4 5 7 nf3an ⊢ Ⅎ z a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b
9 nfv ⊢ Ⅎ z c ∈ ℝ
10 nfv ⊢ Ⅎ z d ∈ ℝ
11 nfrab1 ⊢ Ⅎ _ z z ∈ ℝ | c ≤ z ∧ z < d
12 11 nfeq2 ⊢ Ⅎ z y = z ∈ ℝ | c ≤ z ∧ z < d
13 9 10 12 nf3an ⊢ Ⅎ z c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d
14 8 13 nfan ⊢ Ⅎ z a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d
15 nfv ⊢ Ⅎ z a ≤ c ∧ b ≤ d
16 14 15 nfan ⊢ Ⅎ z a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d
17 nfcv ⊢ Ⅎ _ z x ∩ y
18 nfrab1 ⊢ Ⅎ _ z z ∈ ℝ | c ≤ z ∧ z < b
19 simp3 ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b → x = z ∈ ℝ | a ≤ z ∧ z < b
20 simp3 ⊢ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → y = z ∈ ℝ | c ≤ z ∧ z < d
21 elin ⊢ z ∈ x ∩ y ↔ z ∈ x ∧ z ∈ y
22 eleq2 ⊢ x = z ∈ ℝ | a ≤ z ∧ z < b → z ∈ x ↔ z ∈ z ∈ ℝ | a ≤ z ∧ z < b
23 rabid ⊢ z ∈ z ∈ ℝ | a ≤ z ∧ z < b ↔ z ∈ ℝ ∧ a ≤ z ∧ z < b
24 22 23 bitrdi ⊢ x = z ∈ ℝ | a ≤ z ∧ z < b → z ∈ x ↔ z ∈ ℝ ∧ a ≤ z ∧ z < b
25 24 anbi1d ⊢ x = z ∈ ℝ | a ≤ z ∧ z < b → z ∈ x ∧ z ∈ y ↔ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ z ∈ y
26 21 25 syl5bb ⊢ x = z ∈ ℝ | a ≤ z ∧ z < b → z ∈ x ∩ y ↔ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ z ∈ y
27 eleq2 ⊢ y = z ∈ ℝ | c ≤ z ∧ z < d → z ∈ y ↔ z ∈ z ∈ ℝ | c ≤ z ∧ z < d
28 rabid ⊢ z ∈ z ∈ ℝ | c ≤ z ∧ z < d ↔ z ∈ ℝ ∧ c ≤ z ∧ z < d
29 27 28 bitrdi ⊢ y = z ∈ ℝ | c ≤ z ∧ z < d → z ∈ y ↔ z ∈ ℝ ∧ c ≤ z ∧ z < d
30 29 anbi2d ⊢ y = z ∈ ℝ | c ≤ z ∧ z < d → z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ z ∈ y ↔ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ z ∈ ℝ ∧ c ≤ z ∧ z < d
31 26 30 sylan9bb ⊢ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → z ∈ x ∩ y ↔ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ z ∈ ℝ ∧ c ≤ z ∧ z < d
32 an4 ⊢ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ z ∈ ℝ ∧ c ≤ z ∧ z < d ↔ z ∈ ℝ ∧ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d
33 anidm ⊢ z ∈ ℝ ∧ z ∈ ℝ ↔ z ∈ ℝ
34 33 anbi1i ⊢ z ∈ ℝ ∧ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d ↔ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d
35 32 34 bitri ⊢ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ z ∈ ℝ ∧ c ≤ z ∧ z < d ↔ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d
36 31 35 bitrdi ⊢ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → z ∈ x ∩ y ↔ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d
37 19 20 36 syl2an ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → z ∈ x ∩ y ↔ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d
38 37 adantr ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → z ∈ x ∩ y ↔ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d
39 simpl ⊢ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d → z ∈ ℝ
40 simprrl ⊢ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d → c ≤ z
41 simprlr ⊢ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d → z < b
42 39 40 41 jca32 ⊢ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d → z ∈ ℝ ∧ c ≤ z ∧ z < b
43 38 42 syl6bi ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → z ∈ x ∩ y → z ∈ ℝ ∧ c ≤ z ∧ z < b
44 3simpa ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b → a ∈ ℝ ∧ b ∈ ℝ
45 3simpa ⊢ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → c ∈ ℝ ∧ d ∈ ℝ
46 44 45 anim12i ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → a ∈ ℝ ∧ b ∈ ℝ ∧ c ∈ ℝ ∧ d ∈ ℝ
47 letr ⊢ a ∈ ℝ ∧ c ∈ ℝ ∧ z ∈ ℝ → a ≤ c ∧ c ≤ z → a ≤ z
48 47 3expia ⊢ a ∈ ℝ ∧ c ∈ ℝ → z ∈ ℝ → a ≤ c ∧ c ≤ z → a ≤ z
49 48 exp4a ⊢ a ∈ ℝ ∧ c ∈ ℝ → z ∈ ℝ → a ≤ c → c ≤ z → a ≤ z
50 49 ad2ant2r ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ c ∈ ℝ ∧ d ∈ ℝ → z ∈ ℝ → a ≤ c → c ≤ z → a ≤ z
51 ltletr ⊢ z ∈ ℝ ∧ b ∈ ℝ ∧ d ∈ ℝ → z < b ∧ b ≤ d → z < d
52 51 3coml ⊢ b ∈ ℝ ∧ d ∈ ℝ ∧ z ∈ ℝ → z < b ∧ b ≤ d → z < d
53 52 expcomd ⊢ b ∈ ℝ ∧ d ∈ ℝ ∧ z ∈ ℝ → b ≤ d → z < b → z < d
54 53 3expia ⊢ b ∈ ℝ ∧ d ∈ ℝ → z ∈ ℝ → b ≤ d → z < b → z < d
55 54 ad2ant2l ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ c ∈ ℝ ∧ d ∈ ℝ → z ∈ ℝ → b ≤ d → z < b → z < d
56 50 55 jcad ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ c ∈ ℝ ∧ d ∈ ℝ → z ∈ ℝ → a ≤ c → c ≤ z → a ≤ z ∧ b ≤ d → z < b → z < d
57 anim12 ⊢ a ≤ c → c ≤ z → a ≤ z ∧ b ≤ d → z < b → z < d → a ≤ c ∧ b ≤ d → c ≤ z → a ≤ z ∧ z < b → z < d
58 56 57 syl6 ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ c ∈ ℝ ∧ d ∈ ℝ → z ∈ ℝ → a ≤ c ∧ b ≤ d → c ≤ z → a ≤ z ∧ z < b → z < d
59 58 com23 ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ c ∈ ℝ ∧ d ∈ ℝ → a ≤ c ∧ b ≤ d → z ∈ ℝ → c ≤ z → a ≤ z ∧ z < b → z < d
60 anim12 ⊢ c ≤ z → a ≤ z ∧ z < b → z < d → c ≤ z ∧ z < b → a ≤ z ∧ z < d
61 59 60 syl8 ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ c ∈ ℝ ∧ d ∈ ℝ → a ≤ c ∧ b ≤ d → z ∈ ℝ → c ≤ z ∧ z < b → a ≤ z ∧ z < d
62 61 imp31 ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ a ≤ c ∧ b ≤ d ∧ z ∈ ℝ → c ≤ z ∧ z < b → a ≤ z ∧ z < d
63 62 ancrd ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ a ≤ c ∧ b ≤ d ∧ z ∈ ℝ → c ≤ z ∧ z < b → a ≤ z ∧ z < d ∧ c ≤ z ∧ z < b
64 an42 ⊢ a ≤ z ∧ z < d ∧ c ≤ z ∧ z < b ↔ a ≤ z ∧ c ≤ z ∧ z < b ∧ z < d
65 an4 ⊢ a ≤ z ∧ c ≤ z ∧ z < b ∧ z < d ↔ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d
66 64 65 bitri ⊢ a ≤ z ∧ z < d ∧ c ≤ z ∧ z < b ↔ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d
67 63 66 syl6ib ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ a ≤ c ∧ b ≤ d ∧ z ∈ ℝ → c ≤ z ∧ z < b → a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d
68 simpr ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ a ≤ c ∧ b ≤ d ∧ z ∈ ℝ → z ∈ ℝ
69 67 68 jctild ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ a ≤ c ∧ b ≤ d ∧ z ∈ ℝ → c ≤ z ∧ z < b → z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d
70 46 69 sylanl1 ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d ∧ z ∈ ℝ → c ≤ z ∧ z < b → z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d
71 70 imp ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d ∧ z ∈ ℝ ∧ c ≤ z ∧ z < b → z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d
72 71 an32s ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d ∧ c ≤ z ∧ z < b ∧ z ∈ ℝ → z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d
73 38 adantr ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d ∧ c ≤ z ∧ z < b → z ∈ x ∩ y ↔ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d
74 73 adantr ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d ∧ c ≤ z ∧ z < b ∧ z ∈ ℝ → z ∈ x ∩ y ↔ z ∈ ℝ ∧ a ≤ z ∧ z < b ∧ c ≤ z ∧ z < d
75 72 74 mpbird ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d ∧ c ≤ z ∧ z < b ∧ z ∈ ℝ → z ∈ x ∩ y
76 75 expl ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → c ≤ z ∧ z < b ∧ z ∈ ℝ → z ∈ x ∩ y
77 76 ancomsd ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → z ∈ ℝ ∧ c ≤ z ∧ z < b → z ∈ x ∩ y
78 43 77 impbid ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → z ∈ x ∩ y ↔ z ∈ ℝ ∧ c ≤ z ∧ z < b
79 rabid ⊢ z ∈ z ∈ ℝ | c ≤ z ∧ z < b ↔ z ∈ ℝ ∧ c ≤ z ∧ z < b
80 78 79 bitr4di ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → z ∈ x ∩ y ↔ z ∈ z ∈ ℝ | c ≤ z ∧ z < b
81 16 17 18 80 eqrd ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → x ∩ y = z ∈ ℝ | c ≤ z ∧ z < b
82 3 81 jca ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → b ∈ ℝ ∧ x ∩ y = z ∈ ℝ | c ≤ z ∧ z < b
83 82 19.8ad ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → ∃ b b ∈ ℝ ∧ x ∩ y = z ∈ ℝ | c ≤ z ∧ z < b
84 df-rex ⊢ ∃ b ∈ ℝ x ∩ y = z ∈ ℝ | c ≤ z ∧ z < b ↔ ∃ b b ∈ ℝ ∧ x ∩ y = z ∈ ℝ | c ≤ z ∧ z < b
85 83 84 sylibr ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → ∃ b ∈ ℝ x ∩ y = z ∈ ℝ | c ≤ z ∧ z < b
86 2 85 jca ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → c ∈ ℝ ∧ ∃ b ∈ ℝ x ∩ y = z ∈ ℝ | c ≤ z ∧ z < b
87 86 19.8ad ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → ∃ c c ∈ ℝ ∧ ∃ b ∈ ℝ x ∩ y = z ∈ ℝ | c ≤ z ∧ z < b
88 df-rex ⊢ ∃ c ∈ ℝ ∃ b ∈ ℝ x ∩ y = z ∈ ℝ | c ≤ z ∧ z < b ↔ ∃ c c ∈ ℝ ∧ ∃ b ∈ ℝ x ∩ y = z ∈ ℝ | c ≤ z ∧ z < b
89 87 88 sylibr ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → ∃ c ∈ ℝ ∃ b ∈ ℝ x ∩ y = z ∈ ℝ | c ≤ z ∧ z < b
90 1 icoreelrnab ⊢ x ∩ y ∈ I ↔ ∃ c ∈ ℝ ∃ b ∈ ℝ x ∩ y = z ∈ ℝ | c ≤ z ∧ z < b
91 89 90 sylibr ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → x ∩ y ∈ I