Metamath Proof Explorer


Theorem rexanre

Description: Combine two different upper real properties into one. (Contributed by Mario Carneiro, 8-May-2016)

Ref Expression
Assertion rexanre
|- ( A C_ RR -> ( E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) <-> ( E. j e. RR A. k e. A ( j <_ k -> ph ) /\ E. j e. RR A. k e. A ( j <_ k -> ps ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl
 |-  ( ( ph /\ ps ) -> ph )
2 1 imim2i
 |-  ( ( j <_ k -> ( ph /\ ps ) ) -> ( j <_ k -> ph ) )
3 2 ralimi
 |-  ( A. k e. A ( j <_ k -> ( ph /\ ps ) ) -> A. k e. A ( j <_ k -> ph ) )
4 3 reximi
 |-  ( E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) -> E. j e. RR A. k e. A ( j <_ k -> ph ) )
5 simpr
 |-  ( ( ph /\ ps ) -> ps )
6 5 imim2i
 |-  ( ( j <_ k -> ( ph /\ ps ) ) -> ( j <_ k -> ps ) )
7 6 ralimi
 |-  ( A. k e. A ( j <_ k -> ( ph /\ ps ) ) -> A. k e. A ( j <_ k -> ps ) )
8 7 reximi
 |-  ( E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) -> E. j e. RR A. k e. A ( j <_ k -> ps ) )
9 4 8 jca
 |-  ( E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) -> ( E. j e. RR A. k e. A ( j <_ k -> ph ) /\ E. j e. RR A. k e. A ( j <_ k -> ps ) ) )
10 breq1
 |-  ( j = x -> ( j <_ k <-> x <_ k ) )
11 10 imbi1d
 |-  ( j = x -> ( ( j <_ k -> ph ) <-> ( x <_ k -> ph ) ) )
12 11 ralbidv
 |-  ( j = x -> ( A. k e. A ( j <_ k -> ph ) <-> A. k e. A ( x <_ k -> ph ) ) )
13 12 cbvrexvw
 |-  ( E. j e. RR A. k e. A ( j <_ k -> ph ) <-> E. x e. RR A. k e. A ( x <_ k -> ph ) )
14 breq1
 |-  ( j = y -> ( j <_ k <-> y <_ k ) )
15 14 imbi1d
 |-  ( j = y -> ( ( j <_ k -> ps ) <-> ( y <_ k -> ps ) ) )
16 15 ralbidv
 |-  ( j = y -> ( A. k e. A ( j <_ k -> ps ) <-> A. k e. A ( y <_ k -> ps ) ) )
17 16 cbvrexvw
 |-  ( E. j e. RR A. k e. A ( j <_ k -> ps ) <-> E. y e. RR A. k e. A ( y <_ k -> ps ) )
18 13 17 anbi12i
 |-  ( ( E. j e. RR A. k e. A ( j <_ k -> ph ) /\ E. j e. RR A. k e. A ( j <_ k -> ps ) ) <-> ( E. x e. RR A. k e. A ( x <_ k -> ph ) /\ E. y e. RR A. k e. A ( y <_ k -> ps ) ) )
19 reeanv
 |-  ( E. x e. RR E. y e. RR ( A. k e. A ( x <_ k -> ph ) /\ A. k e. A ( y <_ k -> ps ) ) <-> ( E. x e. RR A. k e. A ( x <_ k -> ph ) /\ E. y e. RR A. k e. A ( y <_ k -> ps ) ) )
20 18 19 bitr4i
 |-  ( ( E. j e. RR A. k e. A ( j <_ k -> ph ) /\ E. j e. RR A. k e. A ( j <_ k -> ps ) ) <-> E. x e. RR E. y e. RR ( A. k e. A ( x <_ k -> ph ) /\ A. k e. A ( y <_ k -> ps ) ) )
21 ifcl
 |-  ( ( y e. RR /\ x e. RR ) -> if ( x <_ y , y , x ) e. RR )
22 21 ancoms
 |-  ( ( x e. RR /\ y e. RR ) -> if ( x <_ y , y , x ) e. RR )
23 22 adantl
 |-  ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) -> if ( x <_ y , y , x ) e. RR )
24 r19.26
 |-  ( A. k e. A ( ( x <_ k -> ph ) /\ ( y <_ k -> ps ) ) <-> ( A. k e. A ( x <_ k -> ph ) /\ A. k e. A ( y <_ k -> ps ) ) )
25 anim12
 |-  ( ( ( x <_ k -> ph ) /\ ( y <_ k -> ps ) ) -> ( ( x <_ k /\ y <_ k ) -> ( ph /\ ps ) ) )
26 simplrl
 |-  ( ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) /\ k e. A ) -> x e. RR )
27 simplrr
 |-  ( ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) /\ k e. A ) -> y e. RR )
28 simpl
 |-  ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) -> A C_ RR )
29 28 sselda
 |-  ( ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) /\ k e. A ) -> k e. RR )
30 maxle
 |-  ( ( x e. RR /\ y e. RR /\ k e. RR ) -> ( if ( x <_ y , y , x ) <_ k <-> ( x <_ k /\ y <_ k ) ) )
31 26 27 29 30 syl3anc
 |-  ( ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) /\ k e. A ) -> ( if ( x <_ y , y , x ) <_ k <-> ( x <_ k /\ y <_ k ) ) )
32 31 imbi1d
 |-  ( ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) /\ k e. A ) -> ( ( if ( x <_ y , y , x ) <_ k -> ( ph /\ ps ) ) <-> ( ( x <_ k /\ y <_ k ) -> ( ph /\ ps ) ) ) )
33 25 32 syl5ibr
 |-  ( ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) /\ k e. A ) -> ( ( ( x <_ k -> ph ) /\ ( y <_ k -> ps ) ) -> ( if ( x <_ y , y , x ) <_ k -> ( ph /\ ps ) ) ) )
34 33 ralimdva
 |-  ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) -> ( A. k e. A ( ( x <_ k -> ph ) /\ ( y <_ k -> ps ) ) -> A. k e. A ( if ( x <_ y , y , x ) <_ k -> ( ph /\ ps ) ) ) )
35 24 34 syl5bir
 |-  ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) -> ( ( A. k e. A ( x <_ k -> ph ) /\ A. k e. A ( y <_ k -> ps ) ) -> A. k e. A ( if ( x <_ y , y , x ) <_ k -> ( ph /\ ps ) ) ) )
36 breq1
 |-  ( j = if ( x <_ y , y , x ) -> ( j <_ k <-> if ( x <_ y , y , x ) <_ k ) )
37 36 rspceaimv
 |-  ( ( if ( x <_ y , y , x ) e. RR /\ A. k e. A ( if ( x <_ y , y , x ) <_ k -> ( ph /\ ps ) ) ) -> E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) )
38 23 35 37 syl6an
 |-  ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) -> ( ( A. k e. A ( x <_ k -> ph ) /\ A. k e. A ( y <_ k -> ps ) ) -> E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) ) )
39 38 rexlimdvva
 |-  ( A C_ RR -> ( E. x e. RR E. y e. RR ( A. k e. A ( x <_ k -> ph ) /\ A. k e. A ( y <_ k -> ps ) ) -> E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) ) )
40 20 39 syl5bi
 |-  ( A C_ RR -> ( ( E. j e. RR A. k e. A ( j <_ k -> ph ) /\ E. j e. RR A. k e. A ( j <_ k -> ps ) ) -> E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) ) )
41 9 40 impbid2
 |-  ( A C_ RR -> ( E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) <-> ( E. j e. RR A. k e. A ( j <_ k -> ph ) /\ E. j e. RR A. k e. A ( j <_ k -> ps ) ) ) )