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 syl5bb ( 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎𝑧𝑧 < 𝑏 ) } → ( 𝑧 ∈ ( 𝑥𝑦 ) ↔ ( ( 𝑧 ∈ ℝ ∧ ( 𝑎𝑧𝑧 < 𝑏 ) ) ∧ 𝑧𝑦 ) ) )
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 syl6bi ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎𝑧𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐𝑧𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎𝑐𝑑𝑏 ) ) → ( 𝑧 ∈ ( 𝑥𝑦 ) → ( 𝑧 ∈ ℝ ∧ ( 𝑐𝑧𝑧 < 𝑑 ) ) ) )
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 syl6ibr ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑎𝑐𝑑𝑏 ) ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝑐𝑧𝑧 < 𝑑 ) → ( ( 𝑎𝑧𝑧 < 𝑑 ) ∧ ( 𝑐𝑧𝑧 < 𝑏 ) ) ) )
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 ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎𝑧𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐𝑧𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎𝑐𝑑𝑏 ) ) → ( 𝑥𝑦 ) ∈ 𝐼 )