Metamath Proof Explorer

Theorem opnvonmbllem1

Description: The half-open interval expressed using a composition of a function (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses opnvonmbllem1.i 
|- F/ i ph
opnvonmbllem1.x 
|- ( ph -> X e. V )
opnvonmbllem1.c 
|- ( ph -> C : X --> QQ )
opnvonmbllem1.d 
|- ( ph -> D : X --> QQ )
opnvonmbllem1.s 
|- ( ph -> X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) C_ B )
opnvonmbllem1.g 
|- ( ph -> B C_ G )
opnvonmbllem1.y 
|- ( ph -> Y e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) )
opnvonmbllem1.k 
|- K = { h e. ( ( QQ X. QQ ) ^m X ) | X_ i e. X ( ( [,) o. h ) ` i ) C_ G }
opnvonmbllem1.h 
|- H = ( i e. X |-> <. ( C ` i ) , ( D ` i ) >. )
Assertion opnvonmbllem1 
|- ( ph -> E. h e. K Y e. X_ i e. X ( ( [,) o. h ) ` i ) )

Proof

Step Hyp Ref Expression
1 opnvonmbllem1.i 
 |-  F/ i ph
2 opnvonmbllem1.x 
 |-  ( ph -> X e. V )
3 opnvonmbllem1.c 
 |-  ( ph -> C : X --> QQ )
4 opnvonmbllem1.d 
 |-  ( ph -> D : X --> QQ )
5 opnvonmbllem1.s 
 |-  ( ph -> X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) C_ B )
6 opnvonmbllem1.g 
 |-  ( ph -> B C_ G )
7 opnvonmbllem1.y 
 |-  ( ph -> Y e. X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) )
8 opnvonmbllem1.k 
 |-  K = { h e. ( ( QQ X. QQ ) ^m X ) | X_ i e. X ( ( [,) o. h ) ` i ) C_ G }
9 opnvonmbllem1.h 
 |-  H = ( i e. X |-> <. ( C ` i ) , ( D ` i ) >. )
10 3 ffvelrnda 
 |-  ( ( ph /\ i e. X ) -> ( C ` i ) e. QQ )
11 4 ffvelrnda 
 |-  ( ( ph /\ i e. X ) -> ( D ` i ) e. QQ )
12 opelxpi 
 |-  ( ( ( C ` i ) e. QQ /\ ( D ` i ) e. QQ ) -> <. ( C ` i ) , ( D ` i ) >. e. ( QQ X. QQ ) )
13 10 11 12 syl2anc 
 |-  ( ( ph /\ i e. X ) -> <. ( C ` i ) , ( D ` i ) >. e. ( QQ X. QQ ) )
14 1 13 9 fmptdf 
 |-  ( ph -> H : X --> ( QQ X. QQ ) )
15 qex 
 |-  QQ e. _V
16 15 15 xpex 
 |-  ( QQ X. QQ ) e. _V
17 16 a1i 
 |-  ( ph -> ( QQ X. QQ ) e. _V )
18 17 2 jca 
 |-  ( ph -> ( ( QQ X. QQ ) e. _V /\ X e. V ) )
19 elmapg 
 |-  ( ( ( QQ X. QQ ) e. _V /\ X e. V ) -> ( H e. ( ( QQ X. QQ ) ^m X ) <-> H : X --> ( QQ X. QQ ) ) )
20 18 19 syl 
 |-  ( ph -> ( H e. ( ( QQ X. QQ ) ^m X ) <-> H : X --> ( QQ X. QQ ) ) )
21 14 20 mpbird 
 |-  ( ph -> H e. ( ( QQ X. QQ ) ^m X ) )
22 1 9 hoi2toco 
 |-  ( ph -> X_ i e. X ( ( [,) o. H ) ` i ) = X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) )
23 5 6 sstrd 
 |-  ( ph -> X_ i e. X ( ( C ` i ) [,) ( D ` i ) ) C_ G )
24 22 23 eqsstrd 
 |-  ( ph -> X_ i e. X ( ( [,) o. H ) ` i ) C_ G )
25 21 24 jca 
 |-  ( ph -> ( H e. ( ( QQ X. QQ ) ^m X ) /\ X_ i e. X ( ( [,) o. H ) ` i ) C_ G ) )
26 nfcv 
 |-  F/_ i h
27 nfmpt1 
 |-  F/_ i ( i e. X |-> <. ( C ` i ) , ( D ` i ) >. )
28 9 27 nfcxfr 
 |-  F/_ i H
29 26 28 nfeq 
 |-  F/ i h = H
30 coeq2 
 |-  ( h = H -> ( [,) o. h ) = ( [,) o. H ) )
31 30 fveq1d 
 |-  ( h = H -> ( ( [,) o. h ) ` i ) = ( ( [,) o. H ) ` i ) )
32 31 adantr 
 |-  ( ( h = H /\ i e. X ) -> ( ( [,) o. h ) ` i ) = ( ( [,) o. H ) ` i ) )
33 29 32 ixpeq2d 
 |-  ( h = H -> X_ i e. X ( ( [,) o. h ) ` i ) = X_ i e. X ( ( [,) o. H ) ` i ) )
34 33 sseq1d 
 |-  ( h = H -> ( X_ i e. X ( ( [,) o. h ) ` i ) C_ G <-> X_ i e. X ( ( [,) o. H ) ` i ) C_ G ) )
35 34 8 elrab2 
 |-  ( H e. K <-> ( H e. ( ( QQ X. QQ ) ^m X ) /\ X_ i e. X ( ( [,) o. H ) ` i ) C_ G ) )
36 25 35 sylibr 
 |-  ( ph -> H e. K )
37 7 22 eleqtrrd 
 |-  ( ph -> Y e. X_ i e. X ( ( [,) o. H ) ` i ) )
38 nfv 
 |-  F/ h Y e. X_ i e. X ( ( [,) o. H ) ` i )
39 nfcv 
 |-  F/_ h H
40 nfrab1 
 |-  F/_ h { h e. ( ( QQ X. QQ ) ^m X ) | X_ i e. X ( ( [,) o. h ) ` i ) C_ G }
41 8 40 nfcxfr 
 |-  F/_ h K
42 33 eleq2d 
 |-  ( h = H -> ( Y e. X_ i e. X ( ( [,) o. h ) ` i ) <-> Y e. X_ i e. X ( ( [,) o. H ) ` i ) ) )
43 38 39 41 42 rspcef 
 |-  ( ( H e. K /\ Y e. X_ i e. X ( ( [,) o. H ) ` i ) ) -> E. h e. K Y e. X_ i e. X ( ( [,) o. h ) ` i ) )
44 36 37 43 syl2anc 
 |-  ( ph -> E. h e. K Y e. X_ i e. X ( ( [,) o. h ) ` i ) )