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 ) ) )