Metamath Proof Explorer

Theorem isbasisrelowllem1

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

Ref Expression
Hypothesis isbasisrelowl.1 
|- I = ( [,) " ( RR X. RR ) )
Assertion isbasisrelowllem1 
|- ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) -> ( x i^i y ) e. I )

Proof

Step Hyp Ref Expression
1 isbasisrelowl.1 
 |-  I = ( [,) " ( RR X. RR ) )
2 simplr1 
 |-  ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) -> c e. RR )
3 simpll2 
 |-  ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) -> b e. RR )
4 nfv 
 |-  F/ z a e. RR
5 nfv 
 |-  F/ z b e. RR
6 nfrab1 
 |-  F/_ z { z e. RR | ( a <_ z /\ z < b ) }
7 6 nfeq2 
 |-  F/ z x = { z e. RR | ( a <_ z /\ z < b ) }
8 4 5 7 nf3an 
 |-  F/ z ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } )
9 nfv 
 |-  F/ z c e. RR
10 nfv 
 |-  F/ z d e. RR
11 nfrab1 
 |-  F/_ z { z e. RR | ( c <_ z /\ z < d ) }
12 11 nfeq2 
 |-  F/ z y = { z e. RR | ( c <_ z /\ z < d ) }
13 9 10 12 nf3an 
 |-  F/ z ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } )
14 8 13 nfan 
 |-  F/ z ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) )
15 nfv 
 |-  F/ z ( a <_ c /\ b <_ d )
16 14 15 nfan 
 |-  F/ z ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) )
17 nfcv 
 |-  F/_ z ( x i^i y )
18 nfrab1 
 |-  F/_ z { z e. RR | ( c <_ z /\ z < b ) }
19 simp3 
 |-  ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) -> x = { z e. RR | ( a <_ z /\ z < b ) } )
20 simp3 
 |-  ( ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) -> y = { z e. RR | ( c <_ z /\ z < d ) } )
21 elin 
 |-  ( z e. ( x i^i y ) <-> ( z e. x /\ z e. y ) )
22 eleq2 
 |-  ( x = { z e. RR | ( a <_ z /\ z < b ) } -> ( z e. x <-> z e. { z e. RR | ( a <_ z /\ z < b ) } ) )
23 rabid 
 |-  ( z e. { z e. RR | ( a <_ z /\ z < b ) } <-> ( z e. RR /\ ( a <_ z /\ z < b ) ) )
24 22 23 bitrdi 
 |-  ( x = { z e. RR | ( a <_ z /\ z < b ) } -> ( z e. x <-> ( z e. RR /\ ( a <_ z /\ z < b ) ) ) )
25 24 anbi1d 
 |-  ( x = { z e. RR | ( a <_ z /\ z < b ) } -> ( ( z e. x /\ z e. y ) <-> ( ( z e. RR /\ ( a <_ z /\ z < b ) ) /\ z e. y ) ) )
26 21 25 bitrid 
 |-  ( x = { z e. RR | ( a <_ z /\ z < b ) } -> ( z e. ( x i^i y ) <-> ( ( z e. RR /\ ( a <_ z /\ z < b ) ) /\ z e. y ) ) )
27 eleq2 
 |-  ( y = { z e. RR | ( c <_ z /\ z < d ) } -> ( z e. y <-> z e. { z e. RR | ( c <_ z /\ z < d ) } ) )
28 rabid 
 |-  ( z e. { z e. RR | ( c <_ z /\ z < d ) } <-> ( z e. RR /\ ( c <_ z /\ z < d ) ) )
29 27 28 bitrdi 
 |-  ( y = { z e. RR | ( c <_ z /\ z < d ) } -> ( z e. y <-> ( z e. RR /\ ( c <_ z /\ z < d ) ) ) )
30 29 anbi2d 
 |-  ( y = { z e. RR | ( c <_ z /\ z < d ) } -> ( ( ( z e. RR /\ ( a <_ z /\ z < b ) ) /\ z e. y ) <-> ( ( z e. RR /\ ( a <_ z /\ z < b ) ) /\ ( z e. RR /\ ( c <_ z /\ z < d ) ) ) ) )
31 26 30 sylan9bb 
 |-  ( ( x = { z e. RR | ( a <_ z /\ z < b ) } /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) -> ( z e. ( x i^i y ) <-> ( ( z e. RR /\ ( a <_ z /\ z < b ) ) /\ ( z e. RR /\ ( c <_ z /\ z < d ) ) ) ) )
32 an4 
 |-  ( ( ( z e. RR /\ ( a <_ z /\ z < b ) ) /\ ( z e. RR /\ ( c <_ z /\ z < d ) ) ) <-> ( ( z e. RR /\ z e. RR ) /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) )
33 anidm 
 |-  ( ( z e. RR /\ z e. RR ) <-> z e. RR )
34 33 anbi1i 
 |-  ( ( ( z e. RR /\ z e. RR ) /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) <-> ( z e. RR /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) )
35 32 34 bitri 
 |-  ( ( ( z e. RR /\ ( a <_ z /\ z < b ) ) /\ ( z e. RR /\ ( c <_ z /\ z < d ) ) ) <-> ( z e. RR /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) )
36 31 35 bitrdi 
 |-  ( ( x = { z e. RR | ( a <_ z /\ z < b ) } /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) -> ( z e. ( x i^i y ) <-> ( z e. RR /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) ) )
37 19 20 36 syl2an 
 |-  ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) -> ( z e. ( x i^i y ) <-> ( z e. RR /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) ) )
38 37 adantr 
 |-  ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) -> ( z e. ( x i^i y ) <-> ( z e. RR /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) ) )
39 simpl 
 |-  ( ( z e. RR /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) -> z e. RR )
40 simprrl 
 |-  ( ( z e. RR /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) -> c <_ z )
41 simprlr 
 |-  ( ( z e. RR /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) -> z < b )
42 39 40 41 jca32 
 |-  ( ( z e. RR /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) -> ( z e. RR /\ ( c <_ z /\ z < b ) ) )
43 38 42 biimtrdi 
 |-  ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) -> ( z e. ( x i^i y ) -> ( z e. RR /\ ( c <_ z /\ z < b ) ) ) )
44 3simpa 
 |-  ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) -> ( a e. RR /\ b e. RR ) )
45 3simpa 
 |-  ( ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) -> ( c e. RR /\ d e. RR ) )
46 44 45 anim12i 
 |-  ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) -> ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) )
47 letr 
 |-  ( ( a e. RR /\ c e. RR /\ z e. RR ) -> ( ( a <_ c /\ c <_ z ) -> a <_ z ) )
48 47 3expia 
 |-  ( ( a e. RR /\ c e. RR ) -> ( z e. RR -> ( ( a <_ c /\ c <_ z ) -> a <_ z ) ) )
49 48 exp4a 
 |-  ( ( a e. RR /\ c e. RR ) -> ( z e. RR -> ( a <_ c -> ( c <_ z -> a <_ z ) ) ) )
50 49 ad2ant2r 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( z e. RR -> ( a <_ c -> ( c <_ z -> a <_ z ) ) ) )
51 ltletr 
 |-  ( ( z e. RR /\ b e. RR /\ d e. RR ) -> ( ( z < b /\ b <_ d ) -> z < d ) )
52 51 3coml 
 |-  ( ( b e. RR /\ d e. RR /\ z e. RR ) -> ( ( z < b /\ b <_ d ) -> z < d ) )
53 52 expcomd 
 |-  ( ( b e. RR /\ d e. RR /\ z e. RR ) -> ( b <_ d -> ( z < b -> z < d ) ) )
54 53 3expia 
 |-  ( ( b e. RR /\ d e. RR ) -> ( z e. RR -> ( b <_ d -> ( z < b -> z < d ) ) ) )
55 54 ad2ant2l 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( z e. RR -> ( b <_ d -> ( z < b -> z < d ) ) ) )
56 50 55 jcad 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( z e. RR -> ( ( 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 e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( z e. RR -> ( ( a <_ c /\ b <_ d ) -> ( ( c <_ z -> a <_ z ) /\ ( z < b -> z < d ) ) ) ) )
59 58 com23 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( ( a <_ c /\ b <_ d ) -> ( z e. RR -> ( ( 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 e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( ( a <_ c /\ b <_ d ) -> ( z e. RR -> ( ( c <_ z /\ z < b ) -> ( a <_ z /\ z < d ) ) ) ) )
62 61 imp31 
 |-  ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) /\ ( a <_ c /\ b <_ d ) ) /\ z e. RR ) -> ( ( c <_ z /\ z < b ) -> ( a <_ z /\ z < d ) ) )
63 62 ancrd 
 |-  ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) /\ ( a <_ c /\ b <_ d ) ) /\ z e. RR ) -> ( ( 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 e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) /\ ( a <_ c /\ b <_ d ) ) /\ z e. RR ) -> ( ( c <_ z /\ z < b ) -> ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) )
68 simpr 
 |-  ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) /\ ( a <_ c /\ b <_ d ) ) /\ z e. RR ) -> z e. RR )
69 67 68 jctild 
 |-  ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) /\ ( a <_ c /\ b <_ d ) ) /\ z e. RR ) -> ( ( c <_ z /\ z < b ) -> ( z e. RR /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) ) )
70 46 69 sylanl1 
 |-  ( ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) /\ z e. RR ) -> ( ( c <_ z /\ z < b ) -> ( z e. RR /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) ) )
71 70 imp 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) /\ z e. RR ) /\ ( c <_ z /\ z < b ) ) -> ( z e. RR /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) )
72 71 an32s 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) /\ ( c <_ z /\ z < b ) ) /\ z e. RR ) -> ( z e. RR /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) )
73 38 adantr 
 |-  ( ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) /\ ( c <_ z /\ z < b ) ) -> ( z e. ( x i^i y ) <-> ( z e. RR /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) ) )
74 73 adantr 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) /\ ( c <_ z /\ z < b ) ) /\ z e. RR ) -> ( z e. ( x i^i y ) <-> ( z e. RR /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) ) )
75 72 74 mpbird 
 |-  ( ( ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) /\ ( c <_ z /\ z < b ) ) /\ z e. RR ) -> z e. ( x i^i y ) )
76 75 expl 
 |-  ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) -> ( ( ( c <_ z /\ z < b ) /\ z e. RR ) -> z e. ( x i^i y ) ) )
77 76 ancomsd 
 |-  ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) -> ( ( z e. RR /\ ( c <_ z /\ z < b ) ) -> z e. ( x i^i y ) ) )
78 43 77 impbid 
 |-  ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) -> ( z e. ( x i^i y ) <-> ( z e. RR /\ ( c <_ z /\ z < b ) ) ) )
79 rabid 
 |-  ( z e. { z e. RR | ( c <_ z /\ z < b ) } <-> ( z e. RR /\ ( c <_ z /\ z < b ) ) )
80 78 79 bitr4di 
 |-  ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) -> ( z e. ( x i^i y ) <-> z e. { z e. RR | ( c <_ z /\ z < b ) } ) )
81 16 17 18 80 eqrd 
 |-  ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) -> ( x i^i y ) = { z e. RR | ( c <_ z /\ z < b ) } )
82 3 81 jca 
 |-  ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) -> ( b e. RR /\ ( x i^i y ) = { z e. RR | ( c <_ z /\ z < b ) } ) )
83 82 19.8ad 
 |-  ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) -> E. b ( b e. RR /\ ( x i^i y ) = { z e. RR | ( c <_ z /\ z < b ) } ) )
84 df-rex 
 |-  ( E. b e. RR ( x i^i y ) = { z e. RR | ( c <_ z /\ z < b ) } <-> E. b ( b e. RR /\ ( x i^i y ) = { z e. RR | ( c <_ z /\ z < b ) } ) )
85 83 84 sylibr 
 |-  ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) -> E. b e. RR ( x i^i y ) = { z e. RR | ( c <_ z /\ z < b ) } )
86 2 85 jca 
 |-  ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) -> ( c e. RR /\ E. b e. RR ( x i^i y ) = { z e. RR | ( c <_ z /\ z < b ) } ) )
87 86 19.8ad 
 |-  ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) -> E. c ( c e. RR /\ E. b e. RR ( x i^i y ) = { z e. RR | ( c <_ z /\ z < b ) } ) )
88 df-rex 
 |-  ( E. c e. RR E. b e. RR ( x i^i y ) = { z e. RR | ( c <_ z /\ z < b ) } <-> E. c ( c e. RR /\ E. b e. RR ( x i^i y ) = { z e. RR | ( c <_ z /\ z < b ) } ) )
89 87 88 sylibr 
 |-  ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) -> E. c e. RR E. b e. RR ( x i^i y ) = { z e. RR | ( c <_ z /\ z < b ) } )
90 1 icoreelrnab 
 |-  ( ( x i^i y ) e. I <-> E. c e. RR E. b e. RR ( x i^i y ) = { z e. RR | ( c <_ z /\ z < b ) } )
91 89 90 sylibr 
 |-  ( ( ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) /\ ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) ) /\ ( a <_ c /\ b <_ d ) ) -> ( x i^i y ) e. I )