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 ⊢Ⅎ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∧d≤b
16 14 15 nfan ⊢Ⅎza∈ℝ∧b∈ℝ∧x=z∈ℝ|a≤z∧z<b∧c∈ℝ∧d∈ℝ∧y=z∈ℝ|c≤z∧z<d∧a≤c∧d≤b
17 nfcv ⊢Ⅎ_zx∩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 bitrdi ⊢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 bitrid ⊢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 bitrdi ⊢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 bitrdi ⊢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 bitr4di ⊢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→∃dd∈ℝ∧x∩y=z∈ℝ|c≤z∧z<d
89 df-rex ⊢∃d∈ℝx∩y=z∈ℝ|c≤z∧z<d↔∃dd∈ℝ∧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→∃cc∈ℝ∧∃d∈ℝx∩y=z∈ℝ|c≤z∧z<d
93 df-rex ⊢∃c∈ℝ∃d∈ℝx∩y=z∈ℝ|c≤z∧z<d↔∃cc∈ℝ∧∃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