Metamath Proof Explorer

Theorem icoreclin

Description: The set of closed-below, open-above intervals of reals is closed under finite intersection. (Contributed by ML, 27-Jul-2020)

Ref Expression
Hypothesis isbasisrelowl.1 ⊢ I = . ℝ 2
Assertion icoreclin ⊢ x ∈ I ∧ y ∈ I → x ∩ y ∈ I

Proof

Step Hyp Ref Expression
1 isbasisrelowl.1 ⊢ I = . ℝ 2
2 1 icoreelrnab ⊢ y ∈ I ↔ ∃ c ∈ ℝ ∃ d ∈ ℝ y = z ∈ ℝ | c ≤ z ∧ z < d
3 1 icoreelrnab ⊢ x ∈ I ↔ ∃ a ∈ ℝ ∃ b ∈ ℝ x = z ∈ ℝ | a ≤ z ∧ z < b
4 1 isbasisrelowllem1 ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ b ≤ d → x ∩ y ∈ I
5 4 ex ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → a ≤ c ∧ b ≤ d → x ∩ y ∈ I
6 1 isbasisrelowllem2 ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ≤ c ∧ d ≤ b → x ∩ y ∈ I
7 6 ex ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → a ≤ c ∧ d ≤ b → x ∩ y ∈ I
8 5 7 jaod ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → a ≤ c ∧ b ≤ d ∨ a ≤ c ∧ d ≤ b → x ∩ y ∈ I
9 incom ⊢ y ∩ x = x ∩ y
10 1 isbasisrelowllem2 ⊢ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ≤ a ∧ b ≤ d → y ∩ x ∈ I
11 9 10 eqeltrrid ⊢ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ≤ a ∧ b ≤ d → x ∩ y ∈ I
12 11 ancom1s ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ c ≤ a ∧ b ≤ d → x ∩ y ∈ I
13 12 ex ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → c ≤ a ∧ b ≤ d → x ∩ y ∈ I
14 1 isbasisrelowllem1 ⊢ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ≤ a ∧ d ≤ b → y ∩ x ∈ I
15 9 14 eqeltrrid ⊢ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ≤ a ∧ d ≤ b → x ∩ y ∈ I
16 15 ancom1s ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d ∧ c ≤ a ∧ d ≤ b → x ∩ y ∈ I
17 16 ex ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → c ≤ a ∧ d ≤ b → x ∩ y ∈ I
18 13 17 jaod ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → c ≤ a ∧ b ≤ d ∨ c ≤ a ∧ d ≤ b → x ∩ y ∈ I
19 3simpa ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b → a ∈ ℝ ∧ b ∈ ℝ
20 3simpa ⊢ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → c ∈ ℝ ∧ d ∈ ℝ
21 letric ⊢ a ∈ ℝ ∧ c ∈ ℝ → a ≤ c ∨ c ≤ a
22 letric ⊢ b ∈ ℝ ∧ d ∈ ℝ → b ≤ d ∨ d ≤ b
23 21 22 anim12i ⊢ a ∈ ℝ ∧ c ∈ ℝ ∧ b ∈ ℝ ∧ d ∈ ℝ → a ≤ c ∨ c ≤ a ∧ b ≤ d ∨ d ≤ b
24 anddi ⊢ a ≤ c ∨ c ≤ a ∧ b ≤ d ∨ d ≤ b ↔ a ≤ c ∧ b ≤ d ∨ a ≤ c ∧ d ≤ b ∨ c ≤ a ∧ b ≤ d ∨ c ≤ a ∧ d ≤ b
25 23 24 sylib ⊢ a ∈ ℝ ∧ c ∈ ℝ ∧ b ∈ ℝ ∧ d ∈ ℝ → a ≤ c ∧ b ≤ d ∨ a ≤ c ∧ d ≤ b ∨ c ≤ a ∧ b ≤ d ∨ c ≤ a ∧ d ≤ b
26 25 an4s ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ c ∈ ℝ ∧ d ∈ ℝ → a ≤ c ∧ b ≤ d ∨ a ≤ c ∧ d ≤ b ∨ c ≤ a ∧ b ≤ d ∨ c ≤ a ∧ d ≤ b
27 19 20 26 syl2an ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → a ≤ c ∧ b ≤ d ∨ a ≤ c ∧ d ≤ b ∨ c ≤ a ∧ b ≤ d ∨ c ≤ a ∧ d ≤ b
28 8 18 27 mpjaod ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b ∧ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → x ∩ y ∈ I
29 28 ex ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ x = z ∈ ℝ | a ≤ z ∧ z < b → c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → x ∩ y ∈ I
30 29 3expia ⊢ a ∈ ℝ ∧ b ∈ ℝ → x = z ∈ ℝ | a ≤ z ∧ z < b → c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → x ∩ y ∈ I
31 30 rexlimivv ⊢ ∃ a ∈ ℝ ∃ b ∈ ℝ x = z ∈ ℝ | a ≤ z ∧ z < b → c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → x ∩ y ∈ I
32 3 31 sylbi ⊢ x ∈ I → c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → x ∩ y ∈ I
33 32 com12 ⊢ c ∈ ℝ ∧ d ∈ ℝ ∧ y = z ∈ ℝ | c ≤ z ∧ z < d → x ∈ I → x ∩ y ∈ I
34 33 3expia ⊢ c ∈ ℝ ∧ d ∈ ℝ → y = z ∈ ℝ | c ≤ z ∧ z < d → x ∈ I → x ∩ y ∈ I
35 34 rexlimivv ⊢ ∃ c ∈ ℝ ∃ d ∈ ℝ y = z ∈ ℝ | c ≤ z ∧ z < d → x ∈ I → x ∩ y ∈ I
36 2 35 sylbi ⊢ y ∈ I → x ∈ I → x ∩ y ∈ I
37 36 impcom ⊢ x ∈ I ∧ y ∈ I → x ∩ y ∈ I