Metamath Proof Explorer

Theorem isbasisrelowllem2

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

Ref Expression
Hypothesis isbasisrelowl.1 
|- I = ( [,) " ( RR X. RR ) )
Assertion isbasisrelowllem2 
|- ( ( ( ( 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 /\ d <_ b ) ) -> ( 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 /\ d <_ b ) ) -> c e. RR )
3 simplr2 
 |-  ( ( ( ( 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 /\ d <_ b ) ) -> d 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 /\ d <_ b )
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 /\ d <_ b ) )
17 nfcv 
 |-  F/_ z ( x i^i y )
18 simp3 
 |-  ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) -> x = { z e. RR | ( a <_ z /\ z < b ) } )
19 simp3 
 |-  ( ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) -> y = { z e. RR | ( c <_ z /\ z < d ) } )
20 elin 
 |-  ( z e. ( x i^i y ) <-> ( z e. x /\ z e. y ) )
21 eleq2 
 |-  ( x = { z e. RR | ( a <_ z /\ z < b ) } -> ( z e. x <-> z e. { z e. RR | ( a <_ z /\ z < b ) } ) )
22 rabid 
 |-  ( z e. { z e. RR | ( a <_ z /\ z < b ) } <-> ( z e. RR /\ ( a <_ z /\ z < b ) ) )
23 21 22 bitrdi 
 |-  ( x = { z e. RR | ( a <_ z /\ z < b ) } -> ( z e. x <-> ( z e. RR /\ ( a <_ z /\ z < b ) ) ) )
24 23 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 ) ) )
25 20 24 syl5bb 
 |-  ( x = { z e. RR | ( a <_ z /\ z < b ) } -> ( z e. ( x i^i y ) <-> ( ( z e. RR /\ ( a <_ z /\ z < b ) ) /\ z e. y ) ) )
26 eleq2 
 |-  ( y = { z e. RR | ( c <_ z /\ z < d ) } -> ( z e. y <-> z e. { z e. RR | ( c <_ z /\ z < d ) } ) )
27 rabid 
 |-  ( z e. { z e. RR | ( c <_ z /\ z < d ) } <-> ( z e. RR /\ ( c <_ z /\ z < d ) ) )
28 26 27 bitrdi 
 |-  ( y = { z e. RR | ( c <_ z /\ z < d ) } -> ( z e. y <-> ( z e. RR /\ ( c <_ z /\ z < d ) ) ) )
29 28 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 ) ) ) ) )
30 25 29 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 ) ) ) ) )
31 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 ) ) ) )
32 anidm 
 |-  ( ( z e. RR /\ z e. RR ) <-> z e. RR )
33 32 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 ) ) ) )
34 31 33 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 ) ) ) )
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 e. RR /\ ( ( a <_ z /\ z < b ) /\ ( c <_ z /\ z < d ) ) ) <-> ( z e. RR /\ ( ( a <_ z /\ z < d ) /\ ( c <_ z /\ z < b ) ) ) )
41 34 40 bitri 
 |-  ( ( ( z e. RR /\ ( a <_ z /\ z < b ) ) /\ ( z e. RR /\ ( c <_ z /\ z < d ) ) ) <-> ( z e. RR /\ ( ( a <_ z /\ z < d ) /\ ( c <_ z /\ z < b ) ) ) )
42 30 41 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 < d ) /\ ( c <_ z /\ z < b ) ) ) ) )
43 18 19 42 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 < d ) /\ ( c <_ z /\ z < b ) ) ) ) )
44 43 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 /\ d <_ b ) ) -> ( z e. ( x i^i y ) <-> ( z e. RR /\ ( ( a <_ z /\ z < d ) /\ ( c <_ z /\ z < b ) ) ) ) )
45 simpl 
 |-  ( ( z e. RR /\ ( ( a <_ z /\ z < d ) /\ ( c <_ z /\ z < b ) ) ) -> z e. RR )
46 simprrl 
 |-  ( ( z e. RR /\ ( ( a <_ z /\ z < d ) /\ ( c <_ z /\ z < b ) ) ) -> c <_ z )
47 simprlr 
 |-  ( ( z e. RR /\ ( ( a <_ z /\ z < d ) /\ ( c <_ z /\ z < b ) ) ) -> z < d )
48 45 46 47 jca32 
 |-  ( ( z e. RR /\ ( ( a <_ z /\ z < d ) /\ ( c <_ z /\ z < b ) ) ) -> ( z e. RR /\ ( c <_ z /\ z < d ) ) )
49 44 48 syl6bi 
 |-  ( ( ( ( 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 /\ d <_ b ) ) -> ( z e. ( x i^i y ) -> ( z e. RR /\ ( c <_ z /\ z < d ) ) ) )
50 3simpa 
 |-  ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) -> ( a e. RR /\ b e. RR ) )
51 3simpa 
 |-  ( ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) -> ( c e. RR /\ d e. RR ) )
52 50 51 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 ) ) )
53 letr 
 |-  ( ( a e. RR /\ c e. RR /\ z e. RR ) -> ( ( a <_ c /\ c <_ z ) -> a <_ z ) )
54 53 3expia 
 |-  ( ( a e. RR /\ c e. RR ) -> ( z e. RR -> ( ( a <_ c /\ c <_ z ) -> a <_ z ) ) )
55 54 exp4a 
 |-  ( ( a e. RR /\ c e. RR ) -> ( z e. RR -> ( a <_ c -> ( c <_ z -> a <_ z ) ) ) )
56 55 ad2ant2r 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( z e. RR -> ( a <_ c -> ( c <_ z -> a <_ z ) ) ) )
57 ltletr 
 |-  ( ( z e. RR /\ d e. RR /\ b e. RR ) -> ( ( z < d /\ d <_ b ) -> z < b ) )
58 57 3com13 
 |-  ( ( b e. RR /\ d e. RR /\ z e. RR ) -> ( ( z < d /\ d <_ b ) -> z < b ) )
59 58 expcomd 
 |-  ( ( b e. RR /\ d e. RR /\ z e. RR ) -> ( d <_ b -> ( z < d -> z < b ) ) )
60 59 3expia 
 |-  ( ( b e. RR /\ d e. RR ) -> ( z e. RR -> ( d <_ b -> ( z < d -> z < b ) ) ) )
61 60 ad2ant2l 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( z e. RR -> ( d <_ b -> ( z < d -> z < b ) ) ) )
62 56 61 jcad 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( z e. RR -> ( ( 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 e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( z e. RR -> ( ( a <_ c /\ d <_ b ) -> ( ( c <_ z -> a <_ z ) /\ ( z < d -> z < b ) ) ) ) )
65 64 com23 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( ( a <_ c /\ d <_ b ) -> ( z e. RR -> ( ( 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 e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( ( a <_ c /\ d <_ b ) -> ( z e. RR -> ( ( c <_ z /\ z < d ) -> ( a <_ z /\ z < b ) ) ) ) )
68 67 imp31 
 |-  ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) /\ ( a <_ c /\ d <_ b ) ) /\ z e. RR ) -> ( ( c <_ z /\ z < d ) -> ( a <_ z /\ z < b ) ) )
69 68 ancrd 
 |-  ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) /\ ( a <_ c /\ d <_ b ) ) /\ z e. RR ) -> ( ( 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 e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) /\ ( a <_ c /\ d <_ b ) ) /\ z e. RR ) -> ( ( c <_ z /\ z < d ) -> ( ( a <_ z /\ z < d ) /\ ( c <_ z /\ z < b ) ) ) )
74 simpr 
 |-  ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) /\ ( a <_ c /\ d <_ b ) ) /\ z e. RR ) -> z e. RR )
75 73 74 jctild 
 |-  ( ( ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) /\ ( a <_ c /\ d <_ b ) ) /\ z e. RR ) -> ( ( c <_ z /\ z < d ) -> ( z e. RR /\ ( ( a <_ z /\ z < d ) /\ ( c <_ z /\ z < b ) ) ) ) )
76 52 75 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 /\ d <_ b ) ) /\ z e. RR ) -> ( ( c <_ z /\ z < d ) -> ( z e. RR /\ ( ( a <_ z /\ z < d ) /\ ( c <_ z /\ z < b ) ) ) ) )
77 76 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 /\ d <_ b ) ) /\ z e. RR ) /\ ( c <_ z /\ z < d ) ) -> ( z e. RR /\ ( ( a <_ z /\ z < d ) /\ ( c <_ z /\ z < b ) ) ) )
78 77 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 /\ d <_ b ) ) /\ ( c <_ z /\ z < d ) ) /\ z e. RR ) -> ( z e. RR /\ ( ( a <_ z /\ z < d ) /\ ( c <_ z /\ z < b ) ) ) )
79 44 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 /\ d <_ b ) ) /\ ( c <_ z /\ z < d ) ) -> ( z e. ( x i^i y ) <-> ( z e. RR /\ ( ( a <_ z /\ z < d ) /\ ( c <_ z /\ z < b ) ) ) ) )
80 79 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 /\ d <_ b ) ) /\ ( c <_ z /\ z < d ) ) /\ z e. RR ) -> ( z e. ( x i^i y ) <-> ( z e. RR /\ ( ( a <_ z /\ z < d ) /\ ( c <_ z /\ z < b ) ) ) ) )
81 78 80 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 /\ d <_ b ) ) /\ ( c <_ z /\ z < d ) ) /\ z e. RR ) -> z e. ( x i^i y ) )
82 81 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 /\ d <_ b ) ) -> ( ( ( c <_ z /\ z < d ) /\ z e. RR ) -> z e. ( x i^i y ) ) )
83 82 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 /\ d <_ b ) ) -> ( ( z e. RR /\ ( c <_ z /\ z < d ) ) -> z e. ( x i^i y ) ) )
84 49 83 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 /\ d <_ b ) ) -> ( z e. ( x i^i y ) <-> ( z e. RR /\ ( c <_ z /\ z < d ) ) ) )
85 84 27 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 /\ d <_ b ) ) -> ( z e. ( x i^i y ) <-> z e. { z e. RR | ( c <_ z /\ z < d ) } ) )
86 16 17 11 85 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 /\ d <_ b ) ) -> ( x i^i y ) = { z e. RR | ( c <_ z /\ z < d ) } )
87 3 86 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 /\ d <_ b ) ) -> ( d e. RR /\ ( x i^i y ) = { z e. RR | ( c <_ z /\ z < d ) } ) )
88 87 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 /\ d <_ b ) ) -> E. d ( d e. RR /\ ( x i^i y ) = { z e. RR | ( c <_ z /\ z < d ) } ) )
89 df-rex 
 |-  ( E. d e. RR ( x i^i y ) = { z e. RR | ( c <_ z /\ z < d ) } <-> E. d ( d e. RR /\ ( x i^i y ) = { z e. RR | ( c <_ z /\ z < d ) } ) )
90 88 89 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 /\ d <_ b ) ) -> E. d e. RR ( x i^i y ) = { z e. RR | ( c <_ z /\ z < d ) } )
91 2 90 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 /\ d <_ b ) ) -> ( c e. RR /\ E. d e. RR ( x i^i y ) = { z e. RR | ( c <_ z /\ z < d ) } ) )
92 91 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 /\ d <_ b ) ) -> E. c ( c e. RR /\ E. d e. RR ( x i^i y ) = { z e. RR | ( c <_ z /\ z < d ) } ) )
93 df-rex 
 |-  ( E. c e. RR E. d e. RR ( x i^i y ) = { z e. RR | ( c <_ z /\ z < d ) } <-> E. c ( c e. RR /\ E. d e. RR ( x i^i y ) = { z e. RR | ( c <_ z /\ z < d ) } ) )
94 92 93 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 /\ d <_ b ) ) -> E. c e. RR E. d e. RR ( x i^i y ) = { z e. RR | ( c <_ z /\ z < d ) } )
95 1 icoreelrnab 
 |-  ( ( x i^i y ) e. I <-> E. c e. RR E. d e. RR ( x i^i y ) = { z e. RR | ( c <_ z /\ z < d ) } )
96 94 95 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 /\ d <_ b ) ) -> ( x i^i y ) e. I )