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 imbitrrid 
 |-  ( ( ( 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 biimtrrid 
 |-  ( ( 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 biimtrid 
 |-  ( 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 ) ) ) )