Metamath Proof Explorer

Theorem isbasisrelowllem1

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

Ref Expression
Hypothesis isbasisrelowl.1 ⊢ 𝐼 = ( [,) “ ( ℝ × ℝ ) )
Assertion isbasisrelowllem1 ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 isbasisrelowl.1 ⊢ 𝐼 = ( [,) “ ( ℝ × ℝ ) )
2 simplr1 ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → 𝑐 ∈ ℝ )
3 simpll2 ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → 𝑏 ∈ ℝ )
4 nfv ⊢ Ⅎ 𝑧 𝑎 ∈ ℝ
5 nfv ⊢ Ⅎ 𝑧 𝑏 ∈ ℝ
6 nfrab1 ⊢ Ⅎ 𝑧 { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) }
7 6 nfeq2 ⊢ Ⅎ 𝑧 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) }
8 4 5 7 nf3an ⊢ Ⅎ 𝑧 ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } )
9 nfv ⊢ Ⅎ 𝑧 𝑐 ∈ ℝ
10 nfv ⊢ Ⅎ 𝑧 𝑑 ∈ ℝ
11 nfrab1 ⊢ Ⅎ 𝑧 { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) }
12 11 nfeq2 ⊢ Ⅎ 𝑧 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) }
13 9 10 12 nf3an ⊢ Ⅎ 𝑧 ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } )
14 8 13 nfan ⊢ Ⅎ 𝑧 ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) )
15 nfv ⊢ Ⅎ 𝑧 ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 )
16 14 15 nfan ⊢ Ⅎ 𝑧 ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) )
17 nfcv ⊢ Ⅎ 𝑧 ( 𝑥 ∩ 𝑦 )
18 nfrab1 ⊢ Ⅎ 𝑧 { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) }
19 simp3 ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) → 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } )
20 simp3 ⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) → 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } )
21 elin ⊢ ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 ∈ 𝑦 ) )
22 eleq2 ⊢ ( 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) )
23 rabid ⊢ ( 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ↔ ( 𝑧 ∈ ℝ ∧ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) )
24 22 23 bitrdi ⊢ ( 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } → ( 𝑧 ∈ 𝑥 ↔ ( 𝑧 ∈ ℝ ∧ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) )
25 24 anbi1d ⊢ ( 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } → ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ∈ 𝑦 ) ↔ ( ( 𝑧 ∈ ℝ ∧ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ∧ 𝑧 ∈ 𝑦 ) ) )
26 21 25 bitrid ⊢ ( 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } → ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ↔ ( ( 𝑧 ∈ ℝ ∧ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ∧ 𝑧 ∈ 𝑦 ) ) )
27 eleq2 ⊢ ( 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) )
28 rabid ⊢ ( 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ↔ ( 𝑧 ∈ ℝ ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) )
29 27 28 bitrdi ⊢ ( 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } → ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ ℝ ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) )
30 29 anbi2d ⊢ ( 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } → ( ( ( 𝑧 ∈ ℝ ∧ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ∧ 𝑧 ∈ 𝑦 ) ↔ ( ( 𝑧 ∈ ℝ ∧ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) ) )
31 26 30 sylan9bb ⊢ ( ( 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) → ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ↔ ( ( 𝑧 ∈ ℝ ∧ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) ) )
32 an4 ⊢ ( ( ( 𝑧 ∈ ℝ ∧ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) ↔ ( ( 𝑧 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) )
33 anidm ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ↔ 𝑧 ∈ ℝ )
34 33 anbi1i ⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) )
35 32 34 bitri ⊢ ( ( ( 𝑧 ∈ ℝ ∧ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) )
36 31 35 bitrdi ⊢ ( ( 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) → ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) ) )
37 19 20 36 syl2an ⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) → ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) ) )
38 37 adantr ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) ) )
39 simpl ⊢ ( ( 𝑧 ∈ ℝ ∧ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) → 𝑧 ∈ ℝ )
40 simprrl ⊢ ( ( 𝑧 ∈ ℝ ∧ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) → 𝑐 ≤ 𝑧 )
41 simprlr ⊢ ( ( 𝑧 ∈ ℝ ∧ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) → 𝑧 < 𝑏 )
42 39 40 41 jca32 ⊢ ( ( 𝑧 ∈ ℝ ∧ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) → ( 𝑧 ∈ ℝ ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) )
43 38 42 biimtrdi ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) → ( 𝑧 ∈ ℝ ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) )
44 3simpa ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) → ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) )
45 3simpa ⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) → ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) )
46 44 45 anim12i ⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) → ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) )
47 letr ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝑎 ≤ 𝑐 ∧ 𝑐 ≤ 𝑧 ) → 𝑎 ≤ 𝑧 ) )
48 47 3expia ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( 𝑧 ∈ ℝ → ( ( 𝑎 ≤ 𝑐 ∧ 𝑐 ≤ 𝑧 ) → 𝑎 ≤ 𝑧 ) ) )
49 48 exp4a ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( 𝑧 ∈ ℝ → ( 𝑎 ≤ 𝑐 → ( 𝑐 ≤ 𝑧 → 𝑎 ≤ 𝑧 ) ) ) )
50 49 ad2ant2r ⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( 𝑧 ∈ ℝ → ( 𝑎 ≤ 𝑐 → ( 𝑐 ≤ 𝑧 → 𝑎 ≤ 𝑧 ) ) ) )
51 ltletr ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( ( 𝑧 < 𝑏 ∧ 𝑏 ≤ 𝑑 ) → 𝑧 < 𝑑 ) )
52 51 3coml ⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝑧 < 𝑏 ∧ 𝑏 ≤ 𝑑 ) → 𝑧 < 𝑑 ) )
53 52 expcomd ⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑏 ≤ 𝑑 → ( 𝑧 < 𝑏 → 𝑧 < 𝑑 ) ) )
54 53 3expia ⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( 𝑧 ∈ ℝ → ( 𝑏 ≤ 𝑑 → ( 𝑧 < 𝑏 → 𝑧 < 𝑑 ) ) ) )
55 54 ad2ant2l ⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( 𝑧 ∈ ℝ → ( 𝑏 ≤ 𝑑 → ( 𝑧 < 𝑏 → 𝑧 < 𝑑 ) ) ) )
56 50 55 jcad ⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( 𝑧 ∈ ℝ → ( ( 𝑎 ≤ 𝑐 → ( 𝑐 ≤ 𝑧 → 𝑎 ≤ 𝑧 ) ) ∧ ( 𝑏 ≤ 𝑑 → ( 𝑧 < 𝑏 → 𝑧 < 𝑑 ) ) ) ) )
57 anim12 ⊢ ( ( ( 𝑎 ≤ 𝑐 → ( 𝑐 ≤ 𝑧 → 𝑎 ≤ 𝑧 ) ) ∧ ( 𝑏 ≤ 𝑑 → ( 𝑧 < 𝑏 → 𝑧 < 𝑑 ) ) ) → ( ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) → ( ( 𝑐 ≤ 𝑧 → 𝑎 ≤ 𝑧 ) ∧ ( 𝑧 < 𝑏 → 𝑧 < 𝑑 ) ) ) )
58 56 57 syl6 ⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( 𝑧 ∈ ℝ → ( ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) → ( ( 𝑐 ≤ 𝑧 → 𝑎 ≤ 𝑧 ) ∧ ( 𝑧 < 𝑏 → 𝑧 < 𝑑 ) ) ) ) )
59 58 com23 ⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) → ( 𝑧 ∈ ℝ → ( ( 𝑐 ≤ 𝑧 → 𝑎 ≤ 𝑧 ) ∧ ( 𝑧 < 𝑏 → 𝑧 < 𝑑 ) ) ) ) )
60 anim12 ⊢ ( ( ( 𝑐 ≤ 𝑧 → 𝑎 ≤ 𝑧 ) ∧ ( 𝑧 < 𝑏 → 𝑧 < 𝑑 ) ) → ( ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) → ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) )
61 59 60 syl8 ⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) → ( 𝑧 ∈ ℝ → ( ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) → ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) ) )
62 61 imp31 ⊢ ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) → ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) )
63 62 ancrd ⊢ ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) → ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) )
64 an42 ⊢ ( ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ↔ ( ( 𝑎 ≤ 𝑧 ∧ 𝑐 ≤ 𝑧 ) ∧ ( 𝑧 < 𝑏 ∧ 𝑧 < 𝑑 ) ) )
65 an4 ⊢ ( ( ( 𝑎 ≤ 𝑧 ∧ 𝑐 ≤ 𝑧 ) ∧ ( 𝑧 < 𝑏 ∧ 𝑧 < 𝑑 ) ) ↔ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) )
66 64 65 bitri ⊢ ( ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ↔ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) )
67 63 66 imbitrdi ⊢ ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) → ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) )
68 simpr ⊢ ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) ∧ 𝑧 ∈ ℝ ) → 𝑧 ∈ ℝ )
69 67 68 jctild ⊢ ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) ) )
70 46 69 sylanl1 ⊢ ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) ) )
71 70 imp ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) )
72 71 an32s ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ∧ 𝑧 ∈ ℝ ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) )
73 38 adantr ⊢ ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) → ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) ) )
74 73 adantr ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ∧ 𝑧 ∈ ℝ ) → ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) ) ) ) )
75 72 74 mpbird ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ∧ 𝑧 ∈ ℝ ) → 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) )
76 75 expl ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → ( ( ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ∧ 𝑧 ∈ ℝ ) → 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) )
77 76 ancomsd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → ( ( 𝑧 ∈ ℝ ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) → 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) )
78 43 77 impbid ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) )
79 rabid ⊢ ( 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ↔ ( 𝑧 ∈ ℝ ∧ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) )
80 78 79 bitr4di ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ↔ 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) )
81 16 17 18 80 eqrd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → ( 𝑥 ∩ 𝑦 ) = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } )
82 3 81 jca ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → ( 𝑏 ∈ ℝ ∧ ( 𝑥 ∩ 𝑦 ) = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) )
83 82 19.8ad ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → ∃ 𝑏 ( 𝑏 ∈ ℝ ∧ ( 𝑥 ∩ 𝑦 ) = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) )
84 df-rex ⊢ ( ∃ 𝑏 ∈ ℝ ( 𝑥 ∩ 𝑦 ) = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ↔ ∃ 𝑏 ( 𝑏 ∈ ℝ ∧ ( 𝑥 ∩ 𝑦 ) = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) )
85 83 84 sylibr ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → ∃ 𝑏 ∈ ℝ ( 𝑥 ∩ 𝑦 ) = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } )
86 2 85 jca ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → ( 𝑐 ∈ ℝ ∧ ∃ 𝑏 ∈ ℝ ( 𝑥 ∩ 𝑦 ) = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) )
87 86 19.8ad ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → ∃ 𝑐 ( 𝑐 ∈ ℝ ∧ ∃ 𝑏 ∈ ℝ ( 𝑥 ∩ 𝑦 ) = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) )
88 df-rex ⊢ ( ∃ 𝑐 ∈ ℝ ∃ 𝑏 ∈ ℝ ( 𝑥 ∩ 𝑦 ) = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ↔ ∃ 𝑐 ( 𝑐 ∈ ℝ ∧ ∃ 𝑏 ∈ ℝ ( 𝑥 ∩ 𝑦 ) = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) )
89 87 88 sylibr ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → ∃ 𝑐 ∈ ℝ ∃ 𝑏 ∈ ℝ ( 𝑥 ∩ 𝑦 ) = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } )
90 1 icoreelrnab ⊢ ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 ↔ ∃ 𝑐 ∈ ℝ ∃ 𝑏 ∈ ℝ ( 𝑥 ∩ 𝑦 ) = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } )
91 89 90 sylibr ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 )