Metamath Proof Explorer

Theorem isbasisrelowllem2

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

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