Metamath Proof Explorer


Theorem rexico

Description: Restrict the base of an upper real quantifier to an upper real set. (Contributed by Mario Carneiro, 12-May-2016)

Ref Expression
Assertion rexico
|- ( ( A C_ RR /\ B e. RR ) -> ( E. j e. ( B [,) +oo ) A. k e. A ( j <_ k -> ph ) <-> E. j e. RR A. k e. A ( j <_ k -> ph ) ) )

Proof

Step Hyp Ref Expression
1 simpr
 |-  ( ( A C_ RR /\ B e. RR ) -> B e. RR )
2 pnfxr
 |-  +oo e. RR*
3 icossre
 |-  ( ( B e. RR /\ +oo e. RR* ) -> ( B [,) +oo ) C_ RR )
4 1 2 3 sylancl
 |-  ( ( A C_ RR /\ B e. RR ) -> ( B [,) +oo ) C_ RR )
5 ssrexv
 |-  ( ( B [,) +oo ) C_ RR -> ( E. j e. ( B [,) +oo ) A. k e. A ( j <_ k -> ph ) -> E. j e. RR A. k e. A ( j <_ k -> ph ) ) )
6 4 5 syl
 |-  ( ( A C_ RR /\ B e. RR ) -> ( E. j e. ( B [,) +oo ) A. k e. A ( j <_ k -> ph ) -> E. j e. RR A. k e. A ( j <_ k -> ph ) ) )
7 simpr
 |-  ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> j e. RR )
8 simplr
 |-  ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> B e. RR )
9 7 8 ifcld
 |-  ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> if ( B <_ j , j , B ) e. RR )
10 max1
 |-  ( ( B e. RR /\ j e. RR ) -> B <_ if ( B <_ j , j , B ) )
11 10 adantll
 |-  ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> B <_ if ( B <_ j , j , B ) )
12 elicopnf
 |-  ( B e. RR -> ( if ( B <_ j , j , B ) e. ( B [,) +oo ) <-> ( if ( B <_ j , j , B ) e. RR /\ B <_ if ( B <_ j , j , B ) ) ) )
13 12 ad2antlr
 |-  ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> ( if ( B <_ j , j , B ) e. ( B [,) +oo ) <-> ( if ( B <_ j , j , B ) e. RR /\ B <_ if ( B <_ j , j , B ) ) ) )
14 9 11 13 mpbir2and
 |-  ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> if ( B <_ j , j , B ) e. ( B [,) +oo ) )
15 simpllr
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) /\ k e. A ) -> B e. RR )
16 simplr
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) /\ k e. A ) -> j e. RR )
17 simpll
 |-  ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> A C_ RR )
18 17 sselda
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) /\ k e. A ) -> k e. RR )
19 maxle
 |-  ( ( B e. RR /\ j e. RR /\ k e. RR ) -> ( if ( B <_ j , j , B ) <_ k <-> ( B <_ k /\ j <_ k ) ) )
20 15 16 18 19 syl3anc
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) /\ k e. A ) -> ( if ( B <_ j , j , B ) <_ k <-> ( B <_ k /\ j <_ k ) ) )
21 simpr
 |-  ( ( B <_ k /\ j <_ k ) -> j <_ k )
22 20 21 syl6bi
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) /\ k e. A ) -> ( if ( B <_ j , j , B ) <_ k -> j <_ k ) )
23 22 imim1d
 |-  ( ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) /\ k e. A ) -> ( ( j <_ k -> ph ) -> ( if ( B <_ j , j , B ) <_ k -> ph ) ) )
24 23 ralimdva
 |-  ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> ( A. k e. A ( j <_ k -> ph ) -> A. k e. A ( if ( B <_ j , j , B ) <_ k -> ph ) ) )
25 breq1
 |-  ( n = if ( B <_ j , j , B ) -> ( n <_ k <-> if ( B <_ j , j , B ) <_ k ) )
26 25 rspceaimv
 |-  ( ( if ( B <_ j , j , B ) e. ( B [,) +oo ) /\ A. k e. A ( if ( B <_ j , j , B ) <_ k -> ph ) ) -> E. n e. ( B [,) +oo ) A. k e. A ( n <_ k -> ph ) )
27 14 24 26 syl6an
 |-  ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> ( A. k e. A ( j <_ k -> ph ) -> E. n e. ( B [,) +oo ) A. k e. A ( n <_ k -> ph ) ) )
28 27 rexlimdva
 |-  ( ( A C_ RR /\ B e. RR ) -> ( E. j e. RR A. k e. A ( j <_ k -> ph ) -> E. n e. ( B [,) +oo ) A. k e. A ( n <_ k -> ph ) ) )
29 breq1
 |-  ( n = j -> ( n <_ k <-> j <_ k ) )
30 29 imbi1d
 |-  ( n = j -> ( ( n <_ k -> ph ) <-> ( j <_ k -> ph ) ) )
31 30 ralbidv
 |-  ( n = j -> ( A. k e. A ( n <_ k -> ph ) <-> A. k e. A ( j <_ k -> ph ) ) )
32 31 cbvrexvw
 |-  ( E. n e. ( B [,) +oo ) A. k e. A ( n <_ k -> ph ) <-> E. j e. ( B [,) +oo ) A. k e. A ( j <_ k -> ph ) )
33 28 32 syl6ib
 |-  ( ( A C_ RR /\ B e. RR ) -> ( E. j e. RR A. k e. A ( j <_ k -> ph ) -> E. j e. ( B [,) +oo ) A. k e. A ( j <_ k -> ph ) ) )
34 6 33 impbid
 |-  ( ( A C_ RR /\ B e. RR ) -> ( E. j e. ( B [,) +oo ) A. k e. A ( j <_ k -> ph ) <-> E. j e. RR A. k e. A ( j <_ k -> ph ) ) )