Metamath Proof Explorer


Theorem axcontlem9

Description: Lemma for axcont . Given the separation assumption, all values of F over A are less than or equal to all values of F over B . (Contributed by Scott Fenton, 20-Jun-2013)

Ref Expression
Hypotheses axcontlem9.1 D=p𝔼N|UBtwnZppBtwnZU
axcontlem9.2 F=xt|xDt0+∞i1Nxi=1tZi+tUi
Assertion axcontlem9 NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUnFAmFBnm

Proof

Step Hyp Ref Expression
1 axcontlem9.1 D=p𝔼N|UBtwnZppBtwnZU
2 axcontlem9.2 F=xt|xDt0+∞i1Nxi=1tZi+tUi
3 simpll NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUN
4 simprl1 NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUZ𝔼N
5 simplr1 NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUA𝔼N
6 simprl2 NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUUA
7 5 6 sseldd NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUU𝔼N
8 simprr NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUZU
9 1 2 axcontlem2 NZ𝔼NU𝔼NZUF:D1-1 onto0+∞
10 3 4 7 8 9 syl31anc NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUF:D1-1 onto0+∞
11 f1ofun F:D1-1 onto0+∞FunF
12 fvelima FunFnFAaAFa=n
13 12 ex FunFnFAaAFa=n
14 10 11 13 3syl NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUnFAaAFa=n
15 fvelima FunFmFBbBFb=m
16 15 ex FunFmFBbBFb=m
17 10 11 16 3syl NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUmFBbBFb=m
18 reeanv aAbBFa=nFb=maAFa=nbBFb=m
19 simplr3 NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUxAyBxBtwnZy
20 breq1 x=axBtwnZyaBtwnZy
21 opeq2 y=bZy=Zb
22 21 breq2d y=baBtwnZyaBtwnZb
23 20 22 rspc2v aAbBxAyBxBtwnZyaBtwnZb
24 19 23 mpan9 NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUaAbBaBtwnZb
25 simplll NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUaAbBN
26 4 adantr NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUaAbBZ𝔼N
27 7 adantr NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUaAbBU𝔼N
28 25 26 27 3jca NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUaAbBNZ𝔼NU𝔼N
29 simplrr NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUaAbBZU
30 1 axcontlem4 NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUAD
31 30 sseld NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUaAaD
32 simpl NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUNA𝔼NB𝔼NxAyBxBtwnZy
33 1 axcontlem3 NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUAZUBD
34 32 4 6 8 33 syl13anc NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUBD
35 34 sseld NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUbBbD
36 31 35 anim12d NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUaAbBaDbD
37 36 imp NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUaAbBaDbD
38 1 2 axcontlem7 NZ𝔼NU𝔼NZUaDbDaBtwnZbFaFb
39 28 29 37 38 syl21anc NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUaAbBaBtwnZbFaFb
40 24 39 mpbid NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUaAbBFaFb
41 breq12 Fa=nFb=mFaFbnm
42 40 41 syl5ibcom NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUaAbBFa=nFb=mnm
43 42 rexlimdvva NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUaAbBFa=nFb=mnm
44 18 43 biimtrrid NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUaAFa=nbBFb=mnm
45 14 17 44 syl2and NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUnFAmFBnm
46 45 ralrimivv NA𝔼NB𝔼NxAyBxBtwnZyZ𝔼NUABZUnFAmFBnm