Metamath Proof Explorer

Theorem icoreclin

Description: The set of closed-below, open-above intervals of reals is closed under finite intersection. (Contributed by ML, 27-Jul-2020)

Ref Expression
Hypothesis isbasisrelowl.1 
|- I = ( [,) " ( RR X. RR ) )
Assertion icoreclin 
|- ( ( x e. I /\ y e. I ) -> ( x i^i y ) e. I )

Proof

Step Hyp Ref Expression
1 isbasisrelowl.1 
 |-  I = ( [,) " ( RR X. RR ) )
2 1 icoreelrnab 
 |-  ( y e. I <-> E. c e. RR E. d e. RR y = { z e. RR | ( c <_ z /\ z < d ) } )
3 1 icoreelrnab 
 |-  ( x e. I <-> E. a e. RR E. b e. RR x = { z e. RR | ( a <_ z /\ z < b ) } )
4 1 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 )
5 4 ex 
 |-  ( ( ( 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 ) )
6 1 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 )
7 6 ex 
 |-  ( ( ( 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 ) )
8 5 7 jaod 
 |-  ( ( ( 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 ) \/ ( a <_ c /\ d <_ b ) ) -> ( x i^i y ) e. I ) )
9 incom 
 |-  ( y i^i x ) = ( x i^i y )
10 1 isbasisrelowllem2 
 |-  ( ( ( ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) /\ ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) ) /\ ( c <_ a /\ b <_ d ) ) -> ( y i^i x ) e. I )
11 9 10 eqeltrrid 
 |-  ( ( ( ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) /\ ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) ) /\ ( c <_ a /\ b <_ d ) ) -> ( x i^i y ) e. I )
12 11 ancom1s 
 |-  ( ( ( ( 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 ) } ) ) /\ ( c <_ a /\ b <_ d ) ) -> ( x i^i y ) e. I )
13 12 ex 
 |-  ( ( ( 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 ) } ) ) -> ( ( c <_ a /\ b <_ d ) -> ( x i^i y ) e. I ) )
14 1 isbasisrelowllem1 
 |-  ( ( ( ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) /\ ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) ) /\ ( c <_ a /\ d <_ b ) ) -> ( y i^i x ) e. I )
15 9 14 eqeltrrid 
 |-  ( ( ( ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) /\ ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) ) /\ ( c <_ a /\ d <_ b ) ) -> ( x i^i y ) e. I )
16 15 ancom1s 
 |-  ( ( ( ( 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 ) } ) ) /\ ( c <_ a /\ d <_ b ) ) -> ( x i^i y ) e. I )
17 16 ex 
 |-  ( ( ( 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 ) } ) ) -> ( ( c <_ a /\ d <_ b ) -> ( x i^i y ) e. I ) )
18 13 17 jaod 
 |-  ( ( ( 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 ) } ) ) -> ( ( ( c <_ a /\ b <_ d ) \/ ( c <_ a /\ d <_ b ) ) -> ( x i^i y ) e. I ) )
19 3simpa 
 |-  ( ( a e. RR /\ b e. RR /\ x = { z e. RR | ( a <_ z /\ z < b ) } ) -> ( a e. RR /\ b e. RR ) )
20 3simpa 
 |-  ( ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) -> ( c e. RR /\ d e. RR ) )
21 letric 
 |-  ( ( a e. RR /\ c e. RR ) -> ( a <_ c \/ c <_ a ) )
22 letric 
 |-  ( ( b e. RR /\ d e. RR ) -> ( b <_ d \/ d <_ b ) )
23 21 22 anim12i 
 |-  ( ( ( a e. RR /\ c e. RR ) /\ ( b e. RR /\ d e. RR ) ) -> ( ( a <_ c \/ c <_ a ) /\ ( b <_ d \/ d <_ b ) ) )
24 anddi 
 |-  ( ( ( a <_ c \/ c <_ a ) /\ ( b <_ d \/ d <_ b ) ) <-> ( ( ( a <_ c /\ b <_ d ) \/ ( a <_ c /\ d <_ b ) ) \/ ( ( c <_ a /\ b <_ d ) \/ ( c <_ a /\ d <_ b ) ) ) )
25 23 24 sylib 
 |-  ( ( ( a e. RR /\ c e. RR ) /\ ( b e. RR /\ d e. RR ) ) -> ( ( ( a <_ c /\ b <_ d ) \/ ( a <_ c /\ d <_ b ) ) \/ ( ( c <_ a /\ b <_ d ) \/ ( c <_ a /\ d <_ b ) ) ) )
26 25 an4s 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( ( ( a <_ c /\ b <_ d ) \/ ( a <_ c /\ d <_ b ) ) \/ ( ( c <_ a /\ b <_ d ) \/ ( c <_ a /\ d <_ b ) ) ) )
27 19 20 26 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 ) } ) ) -> ( ( ( a <_ c /\ b <_ d ) \/ ( a <_ c /\ d <_ b ) ) \/ ( ( c <_ a /\ b <_ d ) \/ ( c <_ a /\ d <_ b ) ) ) )
28 8 18 27 mpjaod 
 |-  ( ( ( 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 ) } ) ) -> ( x i^i y ) e. I )
29 28 ex 
 |-  ( ( 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 ) } ) -> ( x i^i y ) e. I ) )
30 29 3expia 
 |-  ( ( 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 ) } ) -> ( x i^i y ) e. I ) ) )
31 30 rexlimivv 
 |-  ( E. a e. RR E. 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 ) } ) -> ( x i^i y ) e. I ) )
32 3 31 sylbi 
 |-  ( x e. I -> ( ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) -> ( x i^i y ) e. I ) )
33 32 com12 
 |-  ( ( c e. RR /\ d e. RR /\ y = { z e. RR | ( c <_ z /\ z < d ) } ) -> ( x e. I -> ( x i^i y ) e. I ) )
34 33 3expia 
 |-  ( ( c e. RR /\ d e. RR ) -> ( y = { z e. RR | ( c <_ z /\ z < d ) } -> ( x e. I -> ( x i^i y ) e. I ) ) )
35 34 rexlimivv 
 |-  ( E. c e. RR E. d e. RR y = { z e. RR | ( c <_ z /\ z < d ) } -> ( x e. I -> ( x i^i y ) e. I ) )
36 2 35 sylbi 
 |-  ( y e. I -> ( x e. I -> ( x i^i y ) e. I ) )
37 36 impcom 
 |-  ( ( x e. I /\ y e. I ) -> ( x i^i y ) e. I )