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 ⊢Ⅎza∈ℝ
5 nfv ⊢Ⅎzb∈ℝ
6 nfrab1 ⊢Ⅎ_zz∈ℝ|a≤z∧z<b
7 6 nfeq2 ⊢Ⅎzx=z∈ℝ|a≤z∧z<b
8 4 5 7 nf3an ⊢Ⅎza∈ℝ∧b∈ℝ∧x=z∈ℝ|a≤z∧z<b
9 nfv ⊢Ⅎzc∈ℝ
10 nfv ⊢Ⅎzd∈ℝ
11 nfrab1 ⊢Ⅎ_zz∈ℝ|c≤z∧z<d
12 11 nfeq2 ⊢Ⅎzy=z∈ℝ|c≤z∧z<d
13 9 10 12 nf3an ⊢Ⅎzc∈ℝ∧d∈ℝ∧y=z∈ℝ|c≤z∧z<d
14 8 13 nfan ⊢Ⅎza∈ℝ∧b∈ℝ∧x=z∈ℝ|a≤z∧z<b∧c∈ℝ∧d∈ℝ∧y=z∈ℝ|c≤z∧z<d
15 nfv ⊢Ⅎza≤c∧b≤d
16 14 15 nfan ⊢Ⅎza∈ℝ∧b∈ℝ∧x=z∈ℝ|a≤z∧z<b∧c∈ℝ∧d∈ℝ∧y=z∈ℝ|c≤z∧z<d∧a≤c∧b≤d
17 nfcv ⊢Ⅎ_zx∩y
18 nfrab1 ⊢Ⅎ_zz∈ℝ|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 bitrid ⊢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 imbitrdi ⊢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→∃bb∈ℝ∧x∩y=z∈ℝ|c≤z∧z<b
84 df-rex ⊢∃b∈ℝx∩y=z∈ℝ|c≤z∧z<b↔∃bb∈ℝ∧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→∃cc∈ℝ∧∃b∈ℝx∩y=z∈ℝ|c≤z∧z<b
88 df-rex ⊢∃c∈ℝ∃b∈ℝx∩y=z∈ℝ|c≤z∧z<b↔∃cc∈ℝ∧∃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