Metamath Proof Explorer

Theorem isbasisrelowllem2

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

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

Proof

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