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